Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound

Power mean: (Σ_t y_t)² ≤ |T| Σ_t y_t²

For all $\htmlData{mx=1}{T \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{y : \htmlData{mx=0}{T} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{T}}$ ):

\htmlData{mx=4}{\left(\htmlData{mx=3}{\sum_{t} \htmlData{mx=2}{\htmlData{mx=0}{y}(\htmlData{mx=1}{t})}}\right)^{2}} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{\htmlData{mx=8}{\htmlData{mx=7}{\htmlData{mx=5}{\operatorname{card}}(\htmlData{mx=6}{T})}} \cdot \htmlData{mx=13}{\sum_{t} \htmlData{mx=12}{\htmlData{mx=11}{\htmlData{mx=9}{y}(\htmlData{mx=10}{t})}^{2}}}}

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)
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 T. Lean writes f x; papers write f(x). (Fintype T)
⟹Implies: If T, then ℝ. (Between types, A → B is the type of functions from A to B.) (T → ℝ)
aᵇPower: ∑ t, y(t) raised to the power 2. ((∑ t, y t) ^ 2)
≤At most: (∑ t, y(t))^2 is less than or equal to card(T) · (∑ t, y(t)^2). ((∑ t, y t) ^ 2 ≤ (Fintype.card T : ℝ) *…)
∑Summation: Add up y(t) for every t. (∑ t, y t)
RReal numbers: The real numbers: every point on the number line. (ℝ)
(x : T)As real numbers: card(T) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Fintype.card T : ℝ))
·Multiplication: card(T) times ∑ t, y(t)^2. ((Fintype.card T : ℝ) * ∑ t, y t ^ 2)
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)

theorem gq-power-mean {T : Type} [Fintype T] (y : T → ℝ) :
    (∑ t, y t) ^ 2 ≤ (Fintype.card T : ℝ) * ∑ t, y t ^ 2

The step that charges the number of transcripts in the general-query lower bound. Part of Balanced Conversion: the Conversion Theorem's two-way descent factor is exactly 1 + (p−q)²/(q(1−q)), so additive oracle error is second order at mass-balanced nodes; a mass-balanced descent converts any deterministic additive-ε oracle with loss n^{O(ε²)}, and the biased product family shows this is tight. Quantifies the last residual class of the Attention Compute Law.

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: 12 lines of Lean

Power mean: (Σ_t y_t)² ≤ |T| Σ_t y_t²

How it was proved

More proved statements