Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound
Exact two-way chi-square factor: p²/q + (1−p)²/(1−q) = 1 + (p−q)²/(q(1−q))
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
- p, q range over real numbers: the statement must hold for every choice. (
(p q : ℝ)) - <Less than
- 0 is strictly smaller than q. (
0 < q) - aᵇPower
- p raised to the power 2. (
p ^ 2) - a/bDivision
- p^2 divided by q. In Lean, dividing by 0 gives 0. (
p ^ 2 / q) - +Addition
- p^2/q plus (1 − p)^2/(1 − q). (
p ^ 2 / q + (1 - p) ^ 2 / (1 - q)) - =Equality
- p^2/q + (1 − p)^2/(1 − q) and 1 + (p − q)^2/(q · (1 − q)) are the same. (
p ^ 2 / q + (1 - p) ^ 2 / (1 - q) = 1 +…) - -Subtraction
- 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - p) - ·Multiplication
- q times 1 − q. (
q * (1 - q))
theorem bc2-two-way-chi-factor (p q : ℝ) (hq0 : 0 < q) (hq1 : q < 1) :
p ^ 2 / q + (1 - p) ^ 2 / (1 - q) = 1 + (p - q) ^ 2 / (q * (1 - q))At a descent node with true branch mass p and proposal q the chi-square factor is exactly 1 + (p−q)²/(q(1−q)); additive error is second order at balanced nodes and first order only when q is tiny. 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.