Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound
Heavy-exit nodes do not compound: 1 + ε + 4εM ≤ M whenever M ≥ (1+ε)/(1−4ε)
For all , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- ε, M range over real numbers: the statement must hold for every choice. (
(ε M : ℝ)) - ≤At most
- 0 is less than or equal to ε. (
0 ≤ ε) - ·Multiplication
- 4 times ε. (
4 * ε) - <Less than
- 4 · ε is strictly smaller than 1. (
4 * ε < 1) - a/bDivision
- 1 + ε divided by 1 − 4 · ε. In Lean, dividing by 0 gives 0. (
(1 + ε) / (1 - 4 * ε)) - +Addition
- 1 plus ε. (
1 + ε) - -Subtraction
- 1 minus 4 · ε. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - 4 * ε)
theorem bc2-heavy-exit-no-compounding (ε M : ℝ) (hε : 0 ≤ ε) (hε4 : 4 * ε < 1) (hM : (1 + ε) / (1 - 4 * ε) ≤ M) :
1 + ε + 4 * ε * M ≤ MA node whose heavy child is a leaf (ratio ≤ 1+ε) and whose tiny rest branch (mass ≤ 2ε, proposal ε) has X ≤ M satisfies X(v) ≤ M, so unbalanced heavy-exit nodes never raise the tree maximum. 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
Sign in to see the proofThe proof, its signed report and its history.