Result · D-FINITE-INDUCTIVE-CLOSURE

A stable D assignment compiles into a rule

Proved heremachine-checked statementpublication: internal

Meaning

The terminal centres and information metric define a rule reproducing the assignment under the exact theorem’s conditions.

Scientific context

Because a stable terminal state is a Voronoi partition, it compiles: the nearest-centre rule built from the terminal centres and metric reproduces every training label. Duplicate rows inherit the label of the merged atom they belong to.

This is the bridge from asking which labels a fixed sample of observations should get to asking which rule should label an observation not yet seen. It is bookkeeping rather than a second fit: no new optimization runs, and the resulting rule is not an approximation of the partition, it is the partition.

This follows from D-EXCHANGE-IMPLIES-VORONOI by a routine argument. It also carries a weakening the theorem statement itself does not: a real solver stops at a positive gain tolerance, not at zero, so the deployable guarantee is self-consistency at that tolerance — the rule reproduces every training label except on rows whose relocation is worth no more than the tolerance the partition was certified at.

Statement

For distinct positive-weight score atoms obtained by merging duplicate rows, positive-definite retained information, exactly K nonempty cells, and zero-tolerance exact one-point exchange stability, a nearest-centroid rule q_hat(s)=argmin_b (s-mu_b)^T I_hat^{-1}(s-mu_b) exists in positive score dimension, and every such rule reproduces all merged-atom training labels strictly, without a tie breaker.

Assumptions

strictly positive atom weights
coincident score rows merged into distinct atoms
I_q positive definite
exactly K nonempty cells
no relocation constraints beyond preserving nonempty cells
exact zero-gain-tolerance exchange stability
positive score dimension, for the existence half only

bridge from finite assignment to deployable classifier

Where it stops

Bounded by

CE-D-UNMERGED-DUPLICATES-001
One-point exchange stability implies strict self-consistent nearest-centroid assignment even when coincident positive-weight score atoms may be assigned to different cells.

Relationships

Rests on

Finite D exchange stability implies strict self-consistent VoronoiD-EXCHANGE-IMPLIES-VORONOI

The full chain beneath it

Enables

Raises

Consistency of exchange-stable D solutionsOPEN-D-EXCHANGE-CONSISTENCY

Open next door

Machine-checked statement

The statement is proved in Lean 4.33.1 + Mathlib 4.33.1 as ScoreQuantFormal.closure_reproduces_labels. Its hypotheses and conclusion are frozen in a specification file that was audited against this page's statement before the proof was written (verdict: fixes verified with residue). A Lean build certifies the theorem, not the Python and JAX code that implements it.

Frozen specification formal/ScoreQuantFormal/ClosureSpec.lean
Proof module formal/ScoreQuantFormal/Closure.lean
Statement audit
The whole machine-checked chain

In the library

Carried by PartitionResult.compile_quantizer(). Reference (opens in a new tab).

Every object and refusal

Local graph

Prerequisites to the left, what it enables or raises to the right, boundary cases below. Open in the map.

Proof

D6. Exact finite inductive closure / compiler

Every one-point-exchange-stable positive-definite finite D solution with exactly $K$ nonempty cells can be compiled to

\boxed{ \hat q_D(s)= \arg\min_b(s-\mu_b)^\top\widehat I^{-1}(s-\mu_b). }

For merged distinct positive-weight score atoms at exact zero-tolerance stability, this predictor reproduces all training labels exactly, without a tie breaker. Therefore an exact terminal D exchange solution is not merely transductive: it has a canonical deployable extension.

The nonempty-cell hypothesis is load-bearing, not bookkeeping. An empty cell has zero mass, hence the degenerate centroid $0$ , and a training row at the origin is exactly as near to it as to its own centroid: at $d=1$ , $N=2$ , $K=3$ with scores $(-2,0)$ , unit weights and $z=(0,1)$ , the configuration is stable, positive definite and has injective scores, yet row 1 ties between its own cell and the empty one, so a conforming rule may return the empty cell. The statement of D-FINITE-INDUCTIVE-CLOSURE was amended on 7 September 2026 to carry this hypothesis, which D5's node already had.

Original duplicate rows inherit the merged atom's label (D-CLOSURE-DUPLICATE-INHERITANCE): merging preserves cell masses, cell sums, centroids and the retained information, so a rule built from the unmerged data is the same rule. That direction is the content — the unmerged scores are not distinct, so D5 does not apply to them directly.

A finite numerical solver using a positive gain tolerance has a weaker, conditional compiler guarantee (D-COMPILE-TOLERANCE-GUARANTEE, independently audited in AUDITS/AUDIT-D-COMPILE-TOLERANCE-001.md). A complete admissible-move scan bounds individual relocation gains by the tolerance, each priced against the original partition; D5's lower bound alone cannot supply this upper bound. Every positive-weight prediction disagreement must also be admissible. Positive tolerance does not force distinct centroids: a singleton tie can make a disagreement inadmissible, and the library's separate guard refuses it (CE-D-COMPILE-SINGLETON-TIE-001).

There is no bound by this tolerance on simultaneous prediction changes (CE-D-COMPILE-BATCH-TOLERANCE-001), global suboptimality or population loss. Prediction keeps deterministic lowest-index argmin. The implementation uses numerical exact-formula gains in the projected score coordinates, not interval arithmetic; zero-weight rows remain predictable but have no positive-weight label guarantee. This regime is not formalized.

Machine-checked. The exact zero-tolerance statements are ScoreQuantFormal.closure_reproduces_labels and ScoreQuantFormal.closure_duplicates, resting on ScoreQuantFormal.merge_invariance (formal/ScoreQuantFormal/Merge.lean) for the preservation of masses, sums, centroids and information under merging — which is the proof mechanism, carried by no claim node of its own. All in formal/ScoreQuantFormal/Closure.lean, frozen in ClosureSpec.lean and MergeSpec.lean and audited in AUDITS/FORMALIZATION-D-FINITE-INDUCTIVE-CLOSURE-001.md. Not covered: the positive-tolerance guarantee; D5's second duplicate branch, since ClosureDuplicateConclusion assumes the inherited labeling rather than deriving that labels are constant on a duplicate class; and any behaviour of the rule away from the training scores.

From D-optimality · chapter contents