How to read this

Every entity in this record carries one provenance class, drawn as a glyph wherever it is named. The class says where the statement came from and how much authority it has, and shape carries it as well as colour, so the classes stay apart in print and for a reader who does not see the difference between two inks.

Where a statement came from

Established: A published result, used as it stands.
Derived from the literature: A direct translation or synthesis of published results into this setting.
Proved here: Derived in this project and treated as proved internally; not yet publication-audited against the literature.
Proved here, no precedent found: Proved in this project, and a targeted prior-art search found no direct equivalent. A search gap is recorded, not a claim of priority; the nearest prior work is named beside it.
Measured: Supported by numerical evidence only. Never theorem authority.
Counterexample: An explicit example falsifies the stated or generalized claim.
Open: An unresolved question.
Verification record: An independent audit of another result; it carries no result of its own.
Counterexample fixture: A small table of exact rational scores and weights, with the labels and the objective values it produces. It is the arithmetic behind a counterexample, checked by enumeration or by an exact formula rather than by a run.

The machine-checked mark

A glyph with a tick badge marks a statement written in Lean 4 against Mathlib and proved there. The mark is about the statement and never about the implementation: no proof assistant sees the Python or the JAX, and a passing Lean build says nothing about the code that computes with the result. The specification file is frozen and audited on its own before the proof is attempted, so what stands behind the mark is an independent reading of the Lean proposition against the registry statement. The whole track, module by module, is at machine-checked statements.

What a search gap is

Some results are marked as proved here with no direct precedent found. That records the outcome of a targeted search of the literature, run against a written statement of the result: the search found no direct equivalent, and the nearest published work it did find is named on the result's own page. It is a statement about a search, not about priority, and it is not evidence that no equivalent exists. Where a search did find the result, the class says so instead and the source is cited.

How statements are connected

Every edge in the maps and every list on an entity page is one of these relations.

rests on: Proof prerequisite: the source uses the target in its proof.
enables: The source is used by, or directly yields, the target.
raises: The source motivates the target, which is open.
verified by: An independent audit re-derived the source.
references: Reviewed inputs or supporting evidence, not proof prerequisites.
converse fails: The target shows the converse of the source is false.
refuted by: An exact fixture falsifies the source statement.
bounded by: An exact fixture sits on the edge of the source's hypotheses.
cites: The source rests on this published work.

The levels of the problem

A result is stated at one level. The level is what the result is about, and results at different levels do not substitute for one another: what is true of a labelling of one fixed table need not be true of a rule fitted on a sample, and neither settles the design under the population law.

Universal identities: Facts about the information carried by any hard label, before any criterion or solver is chosen.
Score access: How a score is obtained: exact densities, density ratios, or a calibrated classifier, and what each does to the information.
Finite assignment: Labels for a fixed weighted table of scores. The object is the partition itself, not a rule.
Inductive rule from a sample: A rule on score space fitted on a sample and applied to observations not yet seen.
Sample to population: Whether what is optimal on a sample converges to what is optimal under the population law.
Population design: The quantizer that is optimal under the score law itself, with no sample in the way.
Information accounting: How retained information is reported: efficiencies, spectra and direction-resolved diagnostics.
Application: Results stated for a specific use, such as template fits.

The criteria

A result is also stated for one or more criteria, which is what the binning is asked to maximise.

Criterion-independent: Results that hold for every matrix criterion, or that concern the information itself.
D-optimality: Maximises the determinant of the retained information on its informative subspace, weighing every parameter direction at once. The primary criterion of the library and of this research.
Profiled Ds-optimality: Maximises the determinant of the Schur complement for the parameters of interest after the nuisance parameters are profiled out. The second primary criterion; it lacks the D geometry, which is where most of the boundary results live.
Normalised trace: Maximises the trace of the whitened retained information, which is the k-means objective in whitened score space. A control criterion.
A-optimality: Minimises the trace of the inverse information. A control criterion: studied to learn where D-style geometry stops.
E-optimality: Maximises the smallest eigenvalue. A control criterion: the finite geometry fails, which is why the library offers no E solver.

What these pages are

Every page in this section is generated from the project's research registry, the same file the library's own tests read, so a page and the code cannot drift apart without a failing build. The registry is a working record: an entry in it is a statement someone wrote down, together with what it rests on and how far it has been checked. Being in the registry does not by itself publish a claim, and it does not make a claim peer-reviewed; the provenance class on each entity is the whole of what is being asserted about it.

As it stands the record holds 128 statements and 9 verification records, 34 counterexample fixtures, 89 papers of prior work, and 9 statements checked in Lean.