Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound

√ is superadditive on nonnegative finite sums: √(Σx) ≤ Σ√x

For all $\htmlData{mx=1}{T \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{x : \htmlData{mx=0}{T} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall t,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{x}(\htmlData{mx=1}{t})}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{T}}$ ), then

\htmlData{mx=4}{\sqrt{\htmlData{mx=3}{\sum_{t} \htmlData{mx=2}{\htmlData{mx=0}{x}(\htmlData{mx=1}{t})}}}} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{\sum_{t} \htmlData{mx=8}{\sqrt{\htmlData{mx=7}{\htmlData{mx=5}{x}(\htmlData{mx=6}{t})}}}}

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 → ℝ)
∀For all: The statement after the comma holds for every t. (∀ t, 0 ≤ x t)
√Square root: The non-negative number whose square is ∑ t, x(t). (Real.sqrt (∑ t, x t))
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to x(t). (0 ≤ x t)
∑Summation: Add up x(t) for every t. (∑ t, x t)

theorem gq-sqrt-sum-le-sum-sqrt {T : Type} [Fintype T] (x : T → ℝ) (hx : ∀ t, 0 ≤ x t) :
    Real.sqrt (∑ t, x t) ≤ ∑ t, Real.sqrt (x t)

Used to pass from the full family's second moment to the per-transcript fibre second moments 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: 19 lines of Lean

√ is superadditive on nonnegative finite sums: √(Σx) ≤ Σ√x

How it was proved

More proved statements