ScoreQuant

Result · D-LEVERAGE

A cell's D leverage is bounded

Derived from the literaturemachine-checked statementpublication: derived from published

Read the proof and evidence →

Meaning

The leverage inequality constrains cell centres in the inverse retained-information metric.

Scientific context

The supporting inequality behind the exchange-implies-Voronoi argument (D-EXCHANGE-IMPLIES-VORONOI) is a standard projection-leverage bound: for every centroid, a quadratic form against the inverse information matrix is bounded by the reciprocal of the cell's weight, and an analogous bound holds for the difference between two centroids. This is a known result rather than a contribution.

Statement

For every centroid μ_c, μ_c^T I^{-1}μ_c<=1/W_c, and for δ=μ_a-μ_b, δ^T I^{-1}δ<=1/W_a+1/W_b.

Assumptions

  • all K cells nonempty

  • retained information nonsingular, equivalently positive definite

key inequality in finite D geometry

Relationships

Rests on

Enables

Verified by

Open next door

Machine-checked statement

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

Every object and refusal

Local graph
Local map of D leverage inequality1 prerequisites to the left, 2 results it enables or questions it raises to the right, 0 boundary cases below.Quantized Fisher-information identityQuantized Fisher-info…Finite D exchange stability implies strict self-consistent VoronoiFinite D exchange sta…Quantitative D gain lower bound for a Voronoi violationQuantitative D gain l…D leverage inequalityD leverage inequalityPublication-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

D4. Leverage inequality

For every cell centroid,

μc⊤I−1μc≤1/Wc,\mu_c^\top I^{-1}\mu_c\le 1/W_c,

and for centroid difference δ=μa−μb\delta=\mu_a-\mu_b,

δ⊤I−1δ≤1/Wa+1/Wb.\boxed{ \delta^\top I^{-1}\delta \le 1/W_a+1/W_b. }

This is a standard projection/leverage inequality; its role here is to bridge infinitesimal D geometry to exact finite gains.

Explicitly, with

A=[W1μ1,…,WKμK],I=AA⊤,A=[\sqrt{W_1}\mu_1,\ldots,\sqrt{W_K}\mu_K], \qquad I=AA^\top,

the matrix P=A⊤(AA⊤)−1AP=A^\top(AA^\top)^{-1}A is an orthogonal projector. Taking va=1/Wav_a=1/\sqrt{W_a}, vb=−1/Wbv_b=-1/\sqrt{W_b}, and all other coordinates zero gives Av=μa−μbAv=\mu_a-\mu_b, hence

(μa−μb)⊤I−1(μa−μb)=v⊤Pv≤v⊤v=1/Wa+1/Wb.(\mu_a-\mu_b)^\top I^{-1}(\mu_a-\mu_b) =v^\top Pv\le v^\top v=1/W_a+1/W_b.

Machine-checked. Both halves are verified for arbitrary dd in Lean 4.33.1 + Mathlib, via the same projector argument. The bundled statement is frozen in formal/ScoreQuantFormal/LeverageSpec.lean and the proof is ScoreQuantFormal.leverage_inequality in formal/ScoreQuantFormal/Leverage.lean, assembling centroid_leverage_bound and leverage_bound. Independent statement audit: AUDITS/FORMALIZATION-D-LEVERAGE-001.md, verdict match after hardening. Two things that audit established are worth keeping in view. The frozen inequality is true with no hypotheses, because Lean's 0−1=00^{-1}=0 collapses both sides together for an empty cell and a singular II — the hypotheses are fidelity conventions, not guards against falsity, and the proof uses positive definiteness genuinely. And nothing formal connects II to a statistical Fisher information: fisher is defined as ∑cmcmc⊤/Wc\sum_c m_cm_c^\top/W_c, and the identification is inherited from FI-QUANT-IDENTITY, not proved.

From D-optimality · chapter contents