Result · D-EXCHANGE-SCALAR-CORE

A scalar inequality drives the exchange argument

Proved heremachine-checked statementpublication: internal

Meaning

A scalar inequality supplies the core step of the quantitative exchange-to-geometry argument.

Statement

For real w, W_a, W_b, q_aa, q_bb, q_ab with 0<w<W_a, W_b>0, q_aa>=0, q_bb>=0, q_bb<=q_aa, and 0<=q_delta=q_aa+q_bb-2q_ab<=1/W_a+1/W_b, define alpha=wW_a/(W_a-w), beta=wW_b/(W_b+w), and E=alpha q_aa-beta q_bb-alpha beta(q_aa q_bb-q_ab^2). Then E>=alpha beta(q_delta^2+(q_aa-q_bb)^2)/4, hence E>=alpha beta q_delta^2/4, and q_delta>0 implies E>0.

Assumptions

real scalar quantities
0 < source atom weight < source cell mass
positive destination cell mass
nonnegative self quadratic products
q_bb <= q_aa
0 <= q_delta <= 1/W_a + 1/W_b

machine-checked real-arithmetic bridge inside the finite D exchange theorem

Where it stops

This formal proof starts after the matrix/determinant reduction and stops before the logarithm, distinct-centroid, singleton, duplicate-atom, and full Voronoi arguments. Those layers are now machine-checked separately on D-EXCHANGE-IMPLIES-VORONOI; this node remains the scalar lemma they rest on.

Relationships

Enables

Quantitative D gain lower bound for a Voronoi violationD-EXCHANGE-VIOLATION-LOWER-BOUND

Open next door

Machine-checked statement

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

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

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