proofs
Provedattention-compute-lawvariational-cost-lawheadline-theoremsingle-statement

Attention Compute Law, one statement: proposals from side information cost ≥ (Σ_j √E[π_j²|T])², attained by r ∝ √E[π²|T]; uniform optimal when exchangeable; next-step form for adaptive schemes

For all I,J,H∈Type⁡\htmlData{mx=1}{I, J, H \in \htmlData{mx=0}{\operatorname{Type}}}, lam:I→R\htmlData{mx=3}{\mathit{lam} : \htmlData{mx=0}{I} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, a:I→J→R\htmlData{mx=5}{a : \htmlData{mx=0}{I} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{J} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}, r:J→R\htmlData{mx=3}{r : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, Abar∈R\htmlData{mx=1}{\mathit{Abar} \in \htmlData{mx=0}{\mathbb{R}}}, P:H→R\htmlData{mx=3}{P : \htmlData{mx=0}{H} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, lamH:H→I→R\htmlData{mx=5}{\mathit{lamH} : \htmlData{mx=0}{H} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{I} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}} and rH:H→J→R\htmlData{mx=5}{\mathit{rH} : \htmlData{mx=0}{H} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{J} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}, if ∀i, 0≤lam(i)\htmlData{mx=4}{\forall i,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{\mathit{lam}}(\htmlData{mx=1}{i})}}, ∀i,j, 0≤a(i,j)\htmlData{mx=5}{\forall i, j,\ 0 \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\htmlData{mx=0}{a}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})}}, ∀j, 0<r(j)\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}}, ∑jr(j)=1\htmlData{mx=3}{\sum_{j} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}} \mathrel{\htmlData{mx=4}{=}} 1, ∀h, 0≤P(h)\htmlData{mx=4}{\forall h,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{P}(\htmlData{mx=1}{h})}}, ∀h,i, 0≤lamH(h,i)\htmlData{mx=5}{\forall h, i,\ 0 \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\htmlData{mx=0}{\mathit{lamH}}(\htmlData{mx=1}{h}, \htmlData{mx=2}{i})}}, ∀h,j, 0<rH(h,j)\htmlData{mx=5}{\forall h, j,\ 0 \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{\htmlData{mx=0}{\mathit{rH}}(\htmlData{mx=1}{h}, \htmlData{mx=2}{j})}} and ∀h, ∑jrH(h,j)=1\htmlData{mx=6}{\forall h,\ \htmlData{mx=4}{\sum_{j} \htmlData{mx=3}{\htmlData{mx=0}{\mathit{rH}}(\htmlData{mx=1}{h}, \htmlData{mx=2}{j})}} \mathrel{\htmlData{mx=5}{=}} 1} (given Fintype⁡ I\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{I}}, Fintype⁡ J\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}, Nonempty⁡ J\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}} and Fintype⁡ H\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{H}}), then

((∑j∑ilam(i)⋅a(i,j))2≤∑ilam(i)⋅∑ja(i,j)r(j))∧((∀j, 0<∑ilam(i)⋅a(i,j))  ⟹  ∑ilam(i)⋅∑ja(i,j)∑ilam(i)⋅a(i,j)∑k∑ilam(i)⋅a(i,k)=(∑j∑ilam(i)⋅a(i,j))2)∧((∀j, ∑ilam(i)⋅a(i,j)=Abar)  ⟹  card⁡(J)⋅∑j∑ilam(i)⋅a(i,j)≤∑ilam(i)⋅∑ja(i,j)r(j))∧(∑hP(h)⋅(∑j∑ilamH(h,i)⋅a(i,j))2≤∑hP(h)⋅∑ilamH(h,i)⋅∑ja(i,j)rH(h,j))\begin{aligned} & \left(\right. \htmlData{mx=13}{\left(\htmlData{mx=12}{\sum_{j} \htmlData{mx=11}{\sqrt{\htmlData{mx=10}{\sum_{i} \htmlData{mx=9}{\htmlData{mx=4}{\htmlData{mx=2}{\mathit{lam}}(\htmlData{mx=3}{i})} \cdot \htmlData{mx=8}{\htmlData{mx=5}{a}(\htmlData{mx=6}{i}, \htmlData{mx=7}{j})}}}}}}\right)^{2}} \\ & \quad \htmlData{mx=1}{\leq} \htmlData{mx=27}{\sum_{i} \htmlData{mx=26}{\htmlData{mx=16}{\htmlData{mx=14}{\mathit{lam}}(\htmlData{mx=15}{i})} \cdot \htmlData{mx=25}{\sum_{j} \htmlData{mx=24}{\frac{\htmlData{mx=20}{\htmlData{mx=17}{a}(\htmlData{mx=18}{i}, \htmlData{mx=19}{j})}}{\htmlData{mx=23}{\htmlData{mx=21}{r}(\htmlData{mx=22}{j})}}}}}} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \left(\htmlData{mx=39}{\forall j,\ 0 \mathrel{\htmlData{mx=38}{<}} \htmlData{mx=37}{\sum_{i} \htmlData{mx=36}{\htmlData{mx=31}{\htmlData{mx=29}{\mathit{lam}}(\htmlData{mx=30}{i})} \cdot \htmlData{mx=35}{\htmlData{mx=32}{a}(\htmlData{mx=33}{i}, \htmlData{mx=34}{j})}}}}\right) \\ & \htmlData{mx=28}{\implies} \htmlData{mx=73}{\sum_{i} \htmlData{mx=72}{\htmlData{mx=43}{\htmlData{mx=41}{\mathit{lam}}(\htmlData{mx=42}{i})} \cdot \htmlData{mx=71}{\sum_{j} \htmlData{mx=70}{\frac{\htmlData{mx=47}{\htmlData{mx=44}{a}(\htmlData{mx=45}{i}, \htmlData{mx=46}{j})}}{\htmlData{mx=69}{\frac{\htmlData{mx=57}{\sqrt{\htmlData{mx=56}{\sum_{i} \htmlData{mx=55}{\htmlData{mx=50}{\htmlData{mx=48}{\mathit{lam}}(\htmlData{mx=49}{i})} \cdot \htmlData{mx=54}{\htmlData{mx=51}{a}(\htmlData{mx=52}{i}, \htmlData{mx=53}{j})}}}}}}{\htmlData{mx=68}{\sum_{k} \htmlData{mx=67}{\sqrt{\htmlData{mx=66}{\sum_{i} \htmlData{mx=65}{\htmlData{mx=60}{\htmlData{mx=58}{\mathit{lam}}(\htmlData{mx=59}{i})} \cdot \htmlData{mx=64}{\htmlData{mx=61}{a}(\htmlData{mx=62}{i}, \htmlData{mx=63}{k})}}}}}}}}}}}}} \\ & \quad \htmlData{mx=40}{=} \htmlData{mx=85}{\left(\htmlData{mx=84}{\sum_{j} \htmlData{mx=83}{\sqrt{\htmlData{mx=82}{\sum_{i} \htmlData{mx=81}{\htmlData{mx=76}{\htmlData{mx=74}{\mathit{lam}}(\htmlData{mx=75}{i})} \cdot \htmlData{mx=80}{\htmlData{mx=77}{a}(\htmlData{mx=78}{i}, \htmlData{mx=79}{j})}}}}}}\right)^{2}} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \left(\htmlData{mx=98}{\forall j,\ \htmlData{mx=95}{\sum_{i} \htmlData{mx=94}{\htmlData{mx=89}{\htmlData{mx=87}{\mathit{lam}}(\htmlData{mx=88}{i})} \cdot \htmlData{mx=93}{\htmlData{mx=90}{a}(\htmlData{mx=91}{i}, \htmlData{mx=92}{j})}}} \mathrel{\htmlData{mx=97}{=}} \htmlData{mx=96}{\mathit{Abar}}}\right) \\ & \htmlData{mx=86}{\implies} \htmlData{mx=114}{\htmlData{mx=103}{\htmlData{mx=102}{\htmlData{mx=100}{\operatorname{card}}(\htmlData{mx=101}{J})}} \cdot \htmlData{mx=113}{\sum_{j} \htmlData{mx=112}{\sum_{i} \htmlData{mx=111}{\htmlData{mx=106}{\htmlData{mx=104}{\mathit{lam}}(\htmlData{mx=105}{i})} \cdot \htmlData{mx=110}{\htmlData{mx=107}{a}(\htmlData{mx=108}{i}, \htmlData{mx=109}{j})}}}}} \\ & \quad \htmlData{mx=99}{\leq} \htmlData{mx=128}{\sum_{i} \htmlData{mx=127}{\htmlData{mx=117}{\htmlData{mx=115}{\mathit{lam}}(\htmlData{mx=116}{i})} \cdot \htmlData{mx=126}{\sum_{j} \htmlData{mx=125}{\frac{\htmlData{mx=121}{\htmlData{mx=118}{a}(\htmlData{mx=119}{i}, \htmlData{mx=120}{j})}}{\htmlData{mx=124}{\htmlData{mx=122}{r}(\htmlData{mx=123}{j})}}}}}} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=147}{\sum_{h} \htmlData{mx=146}{\htmlData{mx=132}{\htmlData{mx=130}{P}(\htmlData{mx=131}{h})} \cdot \htmlData{mx=145}{\left(\htmlData{mx=144}{\sum_{j} \htmlData{mx=143}{\sqrt{\htmlData{mx=142}{\sum_{i} \htmlData{mx=141}{\htmlData{mx=136}{\htmlData{mx=133}{\mathit{lamH}}(\htmlData{mx=134}{h}, \htmlData{mx=135}{i})} \cdot \htmlData{mx=140}{\htmlData{mx=137}{a}(\htmlData{mx=138}{i}, \htmlData{mx=139}{j})}}}}}}\right)^{2}}}} \\ & \quad \htmlData{mx=129}{\leq} \htmlData{mx=168}{\sum_{h} \htmlData{mx=167}{\htmlData{mx=150}{\htmlData{mx=148}{P}(\htmlData{mx=149}{h})} \cdot \htmlData{mx=166}{\sum_{i} \htmlData{mx=165}{\htmlData{mx=154}{\htmlData{mx=151}{\mathit{lamH}}(\htmlData{mx=152}{h}, \htmlData{mx=153}{i})} \cdot \htmlData{mx=164}{\sum_{j} \htmlData{mx=163}{\frac{\htmlData{mx=158}{\htmlData{mx=155}{a}(\htmlData{mx=156}{i}, \htmlData{mx=157}{j})}}{\htmlData{mx=162}{\htmlData{mx=159}{\mathit{rH}}(\htmlData{mx=160}{h}, \htmlData{mx=161}{j})}}}}}}}} \left.\right) \end{aligned}
What the notation means · or point at any symbol
Type
Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
x ∈ TVariables
I, J, H range over Type: the statement must hold for every choice. ((I J H : Type))
Fintype
Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application
Fintype applied to I. Lean writes f x; papers write f(x). (Fintype I)
Nonempty
Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
⟹Implies
If I, then ℝ. (Between types, A → B is the type of functions from A to B.) (I → ℝ)
∀For all
The statement after the comma holds for every i. (∀ i, 0 ≤ lam i)
∑Summation
Add up r(j) for every j. (∑ j, r j)
=Equality
∑ j, r(j) and 1 are the same. (∑ j, r j = 1)
aᵇPower
∑ j, √(∑ i, lam(i) · a(i, j)) raised to the power 2. ((∑ j, Real.sqrt (∑ i, lam i * a i j)) ^…)
RReal numbers
The real numbers: every point on the number line. (ℝ)
≤At most
0 is less than or equal to lam(i). (0 ≤ lam i)
<Less than
0 is strictly smaller than r(j). (0 < r j)
√Square root
The non-negative number whose square is ∑ i, lam(i) · a(i, j). (Real.sqrt (∑ i, lam i * a i j))
·Multiplication
lam(i) times a(i, j). (lam i * a i j)
a/bDivision
a(i, j) divided by r(j). In Lean, dividing by 0 gives 0. (a i j / r j)
∧And
Both hold: (∀ j, (∑ i, lam(i) · a(i, j)) = Abar) → card(J) · (∑ j, ∑ …, and (∑ h, P(h) · (∑ j, √(∑ i, lamH(h, i) · a(i, j)))^2) ≤ (∑ h…. (((∀ j, ∑ i, lam i * a i j = Abar) → (Fi…)
(x : T)As real numbers
card(J) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Fintype.card J : ℝ))
card
Fintype.card: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype.card)

The strongest provable single statement of the Attention Compute Law. For a row drawn from a finite prior (weights λ over rows, which is the posterior given the side information T a method has) and nonnegative per-key weights a (a = π² for the cost factor; a = π²‖v−g‖² for a residual estimator): (i) every proposal r has expected second-moment factor Σ_i λ_i Σ_j a_ij/r_j ≥ (Σ_j √(Σ_i λ_i a_ij))²; (ii) r_j ∝ √(Σ_i λ_i a_ij) attains it; (iii) if Σ_i λ_i a_ij is the same for every key (exchangeable prior, i.e. nothing is known about where the mass sits) then every proposal costs ≥ |J|·Σ_j E[a_j], which uniform sampling attains, so blind sampling is optimal and costs n·E[Σπ²] = n·E[e^{−H₂}]; (iv) for an adaptive scheme whose proposal after history h is r_h, the expected next-draw cost is ≥ Σ_h P(h)(Σ_j √(Σ_i λ_{h,i} a_ij))². Models: non-adaptive proposals with side information, and the next step of adaptive ones; blind adaptive samplers are covered separately by ua-adaptive-sampling-threshold-explicit. Not claimed: coverage of algorithms outside the proposal model, or the cost of building the optimal proposal. Conjoins vcl-bayes-optimal-proposal, vcl-blind-sampling-optimal-under-exchangeability and vcl-sequential-form.

How it was proved

Proved
5 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
95 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements