A solver that stops early promises less

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.