Provedfisher-cover-lawdecode-attentionexponential-familylaw
Exponential-family χ²: reusing snapshot π_q for π_{q+Δ} costs Σ π_{q+Δ}²/π_q = Z(q) Z(q+2Δ)/Z(q+Δ)²
For all and , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - f(x)Function application
- Fin applied to n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℝ) - x : TVariables
- a, d range over Fin n → ℝ: the statement must hold for every choice. (
(a d : Fin n → ℝ)) - <Less than
- 0 is strictly smaller than n. (
0 < n) - =Equality
- ∑ j, (exp(a(j) + d(j))/(∑ k, exp(a(k) + d(k))))^2/(exp(a(j… and (∑ k, exp(a(k))) · (∑ k, exp(a(k) + 2 · d(k)))/(∑ k, exp(a… are the same. (
∑ j, (Real.exp (a j + d j) / ∑ k, Real.…) - aᵇPower
- exp(a(j) + d(j))/(∑ k, exp(a(k) + d(k))) raised to the power 2. (
(Real.exp (a j + d j) / ∑ k, Real.exp (…) - eˣExponential function
- e raised to the power a(j) + d(j), where e ≈ 2.718. (
Real.exp (a j + d j)) - a/bDivision
- exp(a(j) + d(j)) divided by ∑ k, exp(a(k) + d(k)). In Lean, dividing by 0 gives 0. (
Real.exp (a j + d j) / ∑ k, Real.exp (a…) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - +Addition
- a(j) plus d(j). (
a j + d j) - ∑Summation
- Add up exp(a(k) + d(k)) for every k. (
∑ k, Real.exp (a k + d k)) - ·Multiplication
- 2 times d(k). (
2 * d k)
theorem fc-chi-square-log-partition {n : ℕ} (a d : Fin n → ℝ) (hn : 0 < n) :
∑ j, (Real.exp (a j + d j) / ∑ k, Real.exp (a k + d k)) ^ 2 / (Real.exp (a j) / ∑ k, Real.exp (a k)) = (∑ k, Real.exp (a k)) * (∑ k, Real.exp (a k + 2 * d k)) / (∑ k, Real.exp (a k + d k)) ^ 2Attention rows form an exponential family in the query with sufficient statistic the key; the importance-sampling cost of snapshot reuse is exp of the second difference of the log-partition, locally Δᵀ Cov_{π_q}(k) Δ (the Fisher metric). Classical identity applied to attention reuse. Part of 'Fisher-Cover Law: snapshot reuse is governed by the Fisher geometry of the attention exponential family'.
How it was proved
- Proved
- 4 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 22 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.