Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound
Depth bound: (1 + cε²)^D ≤ exp(cε²D), so the balanced descent loses at most n^{cε²/ln 2} over D = log₂ n levels
For all and , if , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- c, ε range over real numbers: the statement must hold for every choice. (
(c ε : ℝ)) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - ≤At most
- 0 is less than or equal to c. (
0 ≤ c) - +Addition
- 1 plus c · ε^2. (
1 + c * ε ^ 2) - ·Multiplication
- c times ε^2. (
c * ε ^ 2) - aᵇPower
- ε raised to the power 2. (
ε ^ 2) - eˣExponential function
- e raised to the power c · ε^2 · D, where e ≈ 2.718. (
Real.exp (c * ε ^ 2 * D))
theorem bc2-depth-bound (c ε : ℝ) (D : ℕ) (hc : 0 ≤ c) :
(1 + c * ε ^ 2) ^ D ≤ Real.exp (c * ε ^ 2 * D)The compounded second-order loss over the balanced levels is n^{O(ε²)}, against n^{Θ(ε)} for the count-split descent. 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
- 14 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.