Result · D-LOGDET-GAIN

Every D relocation has an exact closed-form gain

Proved heremachine-checked statementpublication: internal

Meaning

A classical determinant identity gives a closed-form gain for the coupled cell-centroid update.

Scientific context

Once the rank-two change to the information matrix (D-RANK2-MOVE) is known, the resulting change in the log determinant has a closed form with no matrix refactorization required. Because every candidate move can be scored this way, a search that accepts only exactly positive gains is strictly monotone on a finite set of labellings, so it cannot cycle and is guaranteed to terminate (D-EXCHANGE-TERMINATES).

The determinant identity behind this closed form is classical. What is transferred here is its application to the between-cell, centroid-coupled update rather than to the within-cluster scatter update used in classical determinant-clustering methods.

Statement

With H=I^{-1}, q_aa=u_a^T H u_a, q_bb=u_b^T H u_b, q_ab=u_a^T H u_b, the determinant ratio is (1+αq_aa)(1-βq_bb)+αβq_ab^2; equivalently ΔF_D=log of that ratio wherever both determinants are positive.

Assumptions

current information symmetric and nonsingular
positive current and candidate determinants for the log-determinant form

exact O(d^2)-type candidate evaluation

Relationships

Rests on

Exact weighted rank-two relocationD-RANK2-MOVE

Enables

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.det_relocation_gain. 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/DetGainSpec.lean
Proof module formal/ScoreQuantFormal/DetGain.lean
Statement audit
The whole machine-checked chain

In the library

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

D3. Exact log-det relocation gain

With $H=I^{-1}$ and

q_{aa}=u_a^\top Hu_a,\quad q_{bb}=u_b^\top Hu_b,\quad q_{ab}=u_a^\top Hu_b,

\boxed{ \Delta F_D =\log\! [(1+\alpha q_{aa})(1-\beta q_{bb})+\alpha\beta q_{ab}^2]. }

Machine-checked. Verified for arbitrary $d$ in Lean 4.33.1 + Mathlib, through the Weinstein-Aronszajn identity. The statement is frozen in formal/ScoreQuantFormal/DetGainSpec.lean and the proof is ScoreQuantFormal.det_relocation_gain in formal/ScoreQuantFormal/DetGain.lean; the underlying determinant identity is det_add_rank_two, and detRatio_eq_one_add_exchangeExcess joins it to the frozen scalar core — that join lives in the editable proof module and is not itself audited. Independent statement audit: AUDITS/FORMALIZATION-D-LOGDET-GAIN-002.md, verdict match after hardening, superseding the first round.

The frozen statement has two components, because this claim is named for a log-determinant gain: the determinant identity, which needs only that $I$ is symmetric and nonsingular and nothing at all of the candidate, and the boxed $\Delta F_D$ form above, which carries the positivity that taking a logarithm needs. The first round found the identity frozen alone, which left the claim covered only in part; the node's assumptions field, which had asked for positive definiteness the identity never uses, was corrected to match.

This supports exact $O(d^2)$ -type candidate evaluation with cached factorizations.

From D-optimality · chapter contents