Machine-checked statements
A machine-checked mark says that the statement of a result has been written in Lean 4 against Mathlib and proved there. It says nothing about the Python implementation: a Lean build certifies a proposition, never the code that computes with it.
The specification file is frozen before the proof is attempted and audited on its own, so the question the audit answers is whether the Lean proposition is the registry statement, and only then does the proof have to go through. The workspace, its build instructions and its conventions are in the formal workspace README.
What is certified
Every declaration above is checked by Lean 4.33.1 + Mathlib 4.33.1.
Outside the track
What the Lean build does not reach, and therefore does not certify:
- Profiled Ds-optimality, whose finite geometry fails and whose certificates are brackets.
- Population measure theory and every sample-to-population limit.
- A solver stopping at a positive tolerance: the exact statements assume no gain is left on the table.
- Geometric realizability is covered only in part, so its claim carries no machine-checked mark.
- The Python and JAX implementation: a Lean build certifies a statement, never the code that computes it.
The proof chain and supporting modules
Each module is proved on the modules before it, so the last statement in the chain rests on every definition that precedes it. A dashed box is a module that is only partly done, and the claims it touches carry no mark.
ConfigWeighted sample, cells, the binned information and the rank-one update identities.
Supporting definitions; it certifies no statement of its own.
RelocationThe exact rank-two relocation identity.
DetGainThe determinant ratio of a relocation, via Weinstein–Aronszajn.
LeverageBoth leverage inequalities.
ScalarExchangeThe frozen scalar core of the exchange theorem.
ExchangeVoronoiExchange stability implies strict Mahalanobis–Voronoi geometry.
MergeMerging repeated rows changes none of the statistics the rule is built from.
Supporting definitions; it certifies no statement of its own.
ClosureA stable assignment compiles into a nearest-centre rule that reproduces every training label.
TerminationAccepting only exact gains ascends, cannot cycle, and stops at a stable assignment.
Corollariesin partRealizability of global optima, in part, and the earlier weaker termination fragments.
CounterexamplesTwo exact boundary witnesses for the exchange theorem.
Supporting definitions; it certifies no statement of its own.
The axioms it is allowed
Every certified declaration is checked to depend on no axiom beyond propext, Classical.choice and Quot.sound, the ordinary classical foundation of Mathlib. Nothing in the chain is admitted by assumption.