Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound

Balanced node: for q ∈ [1/8, 7/8] and |p − q| ≤ ε the two-way factor is ≤ 1 + (64/7) ε²

For all $\htmlData{mx=1}{p, q, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=0}{\frac{1}{8}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{q}$ , $\htmlData{mx=0}{q} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\frac{7}{8}}$ and $\htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{p} - \htmlData{mx=1}{q}} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\varepsilon}$ , then

\htmlData{mx=10}{\htmlData{mx=3}{\frac{\htmlData{mx=1}{\htmlData{mx=0}{p}^{2}}}{\htmlData{mx=2}{q}}} + \htmlData{mx=9}{\frac{\htmlData{mx=6}{(\htmlData{mx=5}{1 - \htmlData{mx=4}{p}})^{2}}}{\htmlData{mx=8}{1 - \htmlData{mx=7}{q}}}}} \mathrel{\htmlData{mx=16}{\leq}} \htmlData{mx=15}{1 + \htmlData{mx=14}{\htmlData{mx=11}{\frac{64}{7}} \cdot \htmlData{mx=13}{\htmlData{mx=12}{\varepsilon}^{2}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: p, q, ε range over real numbers: the statement must hold for every choice. ((p q ε : ℝ))
a/bDivision: 1 divided by 8. In Lean, dividing by 0 gives 0. (1 / 8)
≤At most: 1/8 is less than or equal to q. (1 / 8 ≤ q)
|x|Absolute value: The size of p − q without its sign. (|p - q|)
aᵇPower: p raised to the power 2. (p ^ 2)
+Addition: p^2/q plus (1 − p)^2/(1 − q). (p ^ 2 / q + (1 - p) ^ 2 / (1 - q))
-Subtraction: p minus q. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (p - q)
·Multiplication: 64/7 times ε^2. (64 / 7 * ε ^ 2)

theorem bc2-balanced-factor-bound (p q ε : ℝ) (hq0 : 1 / 8 ≤ q) (hq1 : q ≤ 7 / 8) (hδ : |p - q| ≤ ε) :
    p ^ 2 / q + (1 - p) ^ 2 / (1 - q) ≤ 1 + 64 / 7 * ε ^ 2

The per-level loss of the mass-balanced descent is second order in the oracle's additive error. 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: 25 lines of Lean

Balanced node: for q ∈ [1/8, 7/8] and |p − q| ≤ ε the two-way factor is ≤ 1 + (64/7) ε²

How it was proved

More proved statements