Result · D-EXCHANGE-IMPLIES-VORONOI

Stable D partitions have a geometric rule

Proved heremachine-checked statementindependently auditedpublication: internal

Meaning

Under the theorem’s hypotheses, exact exchange stability forces strict self-consistent nearest-centre geometry.

Scientific context

Take a partition in which no single observation can be moved to another cell with a positive exact information gain. Under stated conditions — coincident score rows merged into one weighted atom, a positive-definite binned information matrix, exactly K nonempty cells, no move restriction beyond keeping cells nonempty, and a zero gain tolerance — that partition is a strict, self-consistent Voronoi partition in the Mahalanobis metric given by the inverse binned information. Any observation sitting in the wrong cell under that rule would have supplied a strictly positive gain, with an explicit lower bound on how large. Distinct cell centres are derived from stability rather than assumed.

This converts a list of labels into a geometric object: without it, a labelling of a sample says nothing about how a new observation should be labelled; with it, the terminal labelling is exactly reproduced by a nearest-centre rule that can be written down and applied later.

No direct precedent was found in a targeted search. The nearest prior work is Telgarsky and Vattani's analysis of Lloyd versus Hartigan fixed points, which studies the same kind of terminal state for sum-of-squared-errors and reaches the opposite conclusion there. The determinant-clustering literature between Friedman and Rubin's 1967 paper and Späth's exchange routines has not been fully swept, including non-English and pre-digital sources, and a Hartigan-style terminal-geometry result for another determinant criterion would count as directly relevant prior work.

Statement

For distinct positive-weight score atoms obtained by merging duplicate rows, positive-definite retained information, exactly K nonempty cells, no move constraints beyond preserving nonempty cells, and zero-tolerance exact stability, every tied-or-worse nearest-centroid comparison from a non-singleton source has strictly positive exact D gain. Stability forces distinct centroids; singleton rows are then strictly nearest to their own centroids. Hence one-point exchange stability implies strict self-consistent D-Voronoi geometry.

Assumptions

strictly positive atom weights
coincident score rows merged, or labels constant on every duplicate class
I_q positive definite
exactly K nonempty cells
no relocation constraints beyond preserving nonempty cells
exact zero-gain-tolerance exchange stability

primary structural theorem

Where it stops

The internal proof has passed the priority-0 audit. The targeted literature search found no direct equivalent, but that search gap is not a novelty/priority claim. The statement is machine-checked in Lean for arbitrary dimension d, on the merged-atoms branch of the duplicate hypothesis only; the alternative 'labels constant on every duplicate class' branch, positive gain tolerances, singular objectives, and any equivalence with the Python/JAX implementation are outside the formalization.

The converse fails

D-Voronoi fixed point does not imply exchange stabilityD-VORONOI-NOT-EXCHANGE

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.

Closest prior work

Nearest prior work

Telgarsky, Vattani (2010)Hartigan's Method: k-means Clustering without Voronoi

Why each source is not this result: the search records

Nearest sources, checked 26 August 2026

Kiefer–Wolfowitz: approximate-design determinant maximization and pointwise sensitivity over a convexified design-measure feasible set; no partition-induced centroids or label-removal update.
Venkitasubramaniam–Tong–Swami: scalar score-function quantization and Fisher-information distortion; no multivariate full-D finite exchange result.
Barnes–Han–Özgür: conditional-score representation and multivariate trace-Fisher geometry; no determinant objective or hard-label relocation theorem.
Dülek: trace-FIM optimal sufficient-statistic quantizers with polytopal cells for exponential families; not the finite full-D exchange implication.
Friedman–Rubin / Späth / Coleman et al.: determinant partition and exchange precedents. The accessible Späth DETEXM source explicitly computes and minimizes a determinant of pooled within-cluster scatter. That objective is not retained between-cell score Fisher information.

The full search record

Relationships

Rests on

The full chain beneath it

Enables

Raises

Verified by

Publication-grade audit of the D exchange theoremAUDIT-D-EXCHANGE-VORONOI

Open next door

Machine-checked statement

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

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

In the library

Carried by GeometryReport. 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

D5. Exchange stability implies strict D-Voronoi geometry

Let coincident score rows be merged into distinct atoms with positive weights, and partition those atoms into exactly $K$ nonempty cells. Assume $I\succ0$ , that the only relocation constraint is preservation of nonempty cells, and that exchange stability means no exact positive-gain relocation (zero gain tolerance). Then a point in a non-singleton source that is tied with or farther from its own centroid than a competing centroid under $I^{-1}$ has

\boxed{ \Delta F_D \ge \log\left(1+\frac{\alpha\beta}{4}q_\delta^2\right)>0 }

when the two centroids are distinct. Here $q_\delta=(\mu_a-\mu_b)^\top I^{-1}(\mu_a-\mu_b)$ .

The exact algebra is

\frac{\det(I+\Delta I)}{\det I}=1+E, \qquad E\ge\frac{\alpha\beta}{4} \left[q_\delta^2+(q_{aa}-q_{bb})^2\right].

Distinct centroids follow from stability rather than needing a separate assumption. If $\mu_a=\mu_b$ and either cell is non-singleton, moving a non-centroid atom between them gives determinant ratio $1+(\alpha-\beta)q_{aa}>1$ . If both are singletons, equality would mean the two score atoms are duplicates, excluded by merging. A singleton atom is then strictly nearest to its own centroid because its own distance is zero and every other centroid is distinct.

Hence

\boxed{ \text{one-point exchange stable} \Rightarrow \text{strict self-consistent D-Voronoi}. }

The converse fails.

Exact ties between distinct centroids are therefore ruled out, not left as an unresolved degeneracy. Split duplicate atoms are a genuine boundary failure: see COUNTEREXAMPLES/CE-D-UNMERGED-DUPLICATES-001.json, machine-checked as ScoreQuantFormal.UnmergedDuplicates.not_strictVoronoi — every hypothesis but injectivity of the score map holds there, and the conclusion fails. Zero-weight rows, singular/pseudodeterminant objectives, extra capacity or mass constraints, and nonzero solver gain tolerances are outside the theorem. At tolerance $\varepsilon>0$ , the implementation certifies only that no geometric disagreement has exact gain exceeding $\varepsilon$ ; strict training-label reproduction need not hold.

Machine-checked. The whole of D5 is verified in Lean 4.33.1 + Mathlib for arbitrary $d$ : the frozen statement boundary is formal/ScoreQuantFormal/ExchangeVoronoiSpec.lean and the proof is ScoreQuantFormal.exchange_voronoi, with the quantitative bound as ScoreQuantFormal.violation_log_gain and its determinant forms violation_lower_bound / violation_strict_gain. Distinct centroids are derived there, as here, by centroid_ne_of_stable. Independent statement audit: AUDITS/FORMALIZATION-D-EXCHANGE-IMPLIES-VORONOI-001.md. The formalization covers the merged-atoms branch of the duplicate hypothesis only, and certifies nothing about the Python/JAX implementation.

Publication-grade audit and proof: AUDITS/AUDIT-D-EXCHANGE-VORONOI-001.md. Exact-rational regression: py/audit_d_exchange_voronoi.py.

From D-optimality · chapter contents

Independently audited. The audit report.