Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound

Truncation depth: after D ≥ 3 log n / log(1/(7/8+ε)) balanced levels a block's mass is ≤ n^{−3}

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{\varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=1}{D \in \htmlData{mx=0}{\mathbb{N}}}$ , if $1 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{n}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\varepsilon}$ , $\htmlData{mx=2}{\htmlData{mx=0}{\frac{7}{8}} + \htmlData{mx=1}{\varepsilon}} \mathrel{\htmlData{mx=3}{<}} 1$ and $\htmlData{mx=8}{\frac{\htmlData{mx=2}{3\htmlData{mx=1}{\log \htmlData{mx=0}{n}}}}{\htmlData{mx=7}{\log \left(\htmlData{mx=6}{\frac{1}{\htmlData{mx=5}{\htmlData{mx=3}{\frac{7}{8}} + \htmlData{mx=4}{\varepsilon}}}}\right)}}} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{D}$ , then

\htmlData{mx=4}{\left(\htmlData{mx=2}{\htmlData{mx=0}{\frac{7}{8}} + \htmlData{mx=1}{\varepsilon}}\right)^{\htmlData{mx=3}{D}}} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\frac{1}{\htmlData{mx=7}{\htmlData{mx=6}{\htmlData{mx=5}{n}}^{3}}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 1 is less than or equal to n. (1 ≤ n)
a/bDivision: 7 divided by 8. In Lean, dividing by 0 gives 0. (7 / 8)
+Addition: 7/8 plus ε. (7 / 8 + ε)
<Less than: 7/8 + ε is strictly smaller than 1. (7 / 8 + ε < 1)
·Multiplication: 3 times log(n). (3 * Real.log n)
aᵇPower: 7/8 + ε raised to the power D. ((7 / 8 + ε) ^ D)
logNatural logarithm: The logarithm of n to base e: the power e must be raised to to give n. (Real.log n)
(x : T)As real numbers: n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((n : ℝ))

theorem bc2-truncation-depth (n : ℕ) (ε : ℝ) (D : ℕ) (hn : 1 ≤ n) (hε : 0 ≤ ε) (hε' : 7 / 8 + ε < 1) (hD : 3 * Real.log n / Real.log (1 / (7 / 8 + ε)) ≤ D) :
    (7 / 8 + ε) ^ D ≤ 1 / (n : ℝ) ^ 3

Bounds the depth of the balanced descent at O(log n) levels, after which blocks are handled by a uniform proposal with negligible total contribution. 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: 26 lines of Lean

Truncation depth: after D ≥ 3 log n / log(1/(7/8+ε)) balanced levels a block's mass is ≤ n^{−3}

How it was proved

More proved statements