ScoreQuant

Result · D-RANK2-MOVE

Relocation changes information by rank two

Proved heremachine-checked statementpublication: internal

Read the proof and evidence →

Meaning

Moving one weighted observation changes the two affected cell contributions through an exact rank-two identity.

Scientific context

Moving one weighted observation from one cell to another changes the binned information matrix by a rank-two update. Because the update has this closed form, every candidate relocation can be scored exactly and cheaply: the solver never has to rebuild and refactorize the information matrix to compare two partitions, and it never accepts a move on the strength of an approximation.

Exchange-method scatter updates of this general kind go back to Späth, and to Friedman and Rubin, and to Scott and Symons. What is new here is the between-cell form with centroid-coupled coefficients, rather than the within-scatter form those methods use — though it remains possible that Späth's exchange routines already contain this same centroid-coupled between-scatter update, which would make this a known result rather than an adaptation of one.

Statement

For a weighted point moved from non-singleton a to b, ΔI=αu_a u_a^T-βu_b u_b^T with α=wW_a/(W_a-w), β=wW_b/(W_b+w).

Assumptions

  • positive weights

  • source remains nonempty

  • destination is a distinct, nonempty cell

exact finite move algebra

Closest prior work

Nearest prior work

Relationships

Enables

Raises

Verified by

Open next door

Machine-checked statement

The statement is proved in Lean 4.33.1 + Mathlib 4.33.1 as ScoreQuantFormal.rank_two_relocation. 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.

In the library

Carried by DExchangeConfig. Reference.

Every object and refusal

Local graph
Local map of Exact weighted rank-two relocation0 prerequisites to the left, 6 results it enables or questions it raises to the right, 0 boundary cases below.Exact finite A move oracleExact finite A move o…Exact finite D log-determinant gainExact finite D log-de…Exact finite Ds one-point objective oracleExact finite Ds one-p…Concavity/supergradient finite-move screeningConcavity/supergradie…Population stationary geometry for profiled DsPopulation stationary…Stronger local neighborhoodsStronger local neighb…Exact weighted rank-two relocationExact weighted rank-t…Publication-grade audit of the D exchange theoremPublication-grade aud…
Prerequisites to the left, what it enables or raises to the right, boundary cases below. Open in the map.

Proof

D2. Exact weighted rank-two relocation

Move weighted point (s,w)(s,w) from a non-singleton source aa to destination bb. Let

ua=s−μa,ub=s−μb,u_a=s-\mu_a,\quad u_b=s-\mu_b, α=wWaWa−w,β=wWbWb+w.\alpha=\frac{wW_a}{W_a-w},\qquad \beta=\frac{wW_b}{W_b+w}.

Then

ΔI=αuaua⊤−βubub⊤.\boxed{ \Delta I =\alpha u_au_a^\top- \beta u_bu_b^\top. }

Machine-checked. Verified for arbitrary dd in Lean 4.33.1 + Mathlib. The statement is frozen in formal/ScoreQuantFormal/RelocationSpec.lean and the proof is ScoreQuantFormal.rank_two_relocation in formal/ScoreQuantFormal/Relocation.lean, whose type is the frozen RelocationConclusion; the underlying identity is fisher_relocate_sub. Independent statement audit: AUDITS/FORMALIZATION-D-RANK2-MOVE-001.md, verdict match after hardening. That audit narrowed the claim node: the formalization requires the destination to be a distinct, nonempty cell, and the node's assumptions now record it.

From D-optimality · chapter contents