Geometry violations have a measurable gain

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.