Provedfisher-cover-lawdecode-attentionexponential-familylaw
Peaked heads are trajectory-easy: peak mass ≥ 1−δ and relative tilts ≤ η give 1 + χ² ≤ (1 + δ e^{2η})/(1−δ)²
For all , , and , if , , , , and , 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
- p, t range over Fin n → ℝ: the statement must hold for every choice. (
(p t : Fin n → ℝ)) - x ∈ TVariables
- δ, η range over real numbers: the statement must hold for every choice. (
(δ η : ℝ)) - ∀For all
- The statement after the comma holds for every j. (
∀ j, 0 ≤ p j) - ∑Summation
- Add up p(j) for every j. (
∑ j, p j) - =Equality
- ∑ j, p(j) and 1 are the same. (
∑ j, p j = 1) - -Subtraction
- 1 minus δ. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - δ) - <Less than
- δ is strictly smaller than 1. (
δ < 1) - a/bDivision
- ∑ j, p(j) · exp(2 · t(j)) divided by (∑ j, p(j) · exp(t(j)))^2. In Lean, dividing by 0 gives 0. (
(∑ j, p j * Real.exp (2 * t j)) / (∑ j,…) - ≤At most
- 0 is less than or equal to p(j). (
0 ≤ p j) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - eˣExponential function
- e raised to the power 2 · t(j), where e ≈ 2.718. (
Real.exp (2 * t j)) - ·Multiplication
- 2 times t(j). (
2 * t j) - aᵇPower
- ∑ j, p(j) · exp(t(j)) raised to the power 2. (
(∑ j, p j * Real.exp (t j)) ^ 2) - +Addition
- 1 plus δ · exp(2 · η). (
1 + δ * Real.exp (2 * η))
theorem fc-peaked-head-chi-square {n : ℕ} (p t : Fin n → ℝ) (j0 : Fin n) (δ η : ℝ) (hp : ∀ j, 0 ≤ p j) (hsum : ∑ j, p j = 1) (hpeak : 1 - δ ≤ p j0) (hδ : δ < 1) (ht0 : t j0 = 0) (ht : ∀ j, t j ≤ η) :
(∑ j, p j * Real.exp (2 * t j)) / (∑ j, p j * Real.exp (t j)) ^ 2 ≤ (1 + δ * Real.exp (2 * η)) / (1 - δ) ^ 2A retrieval head whose focus key is stable can reuse its snapshot at cost ≈ 1 + O(δ e^{2η}) even for large η (where the sup-norm bound e^{2η} is useless): batch-hard heads can be trajectory-easy. 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
- 40 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.