proofs
Provedproposal-principleattentionunifiedcrux

Node inheritance: children masses M₁ + M₀ = M, an additive-ε estimate of M₁/M smoothed to p̃ ⇒ M₁ ≤ (1+2ε)p̃M and M₀ ≤ (1+2ε)(1−p̃)M

For all M,M1,M0,phat,ε∈R\htmlData{mx=1}{M, M_{1}, M_{0}, \mathit{phat}, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}, if 0≤M10 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{M_{1}}, 0≤M00 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{M_{0}}, M1+M0=M\htmlData{mx=2}{\htmlData{mx=0}{M_{1}} + \htmlData{mx=1}{M_{0}}} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{M}, 0<ε0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon} and 0<M  ⟹  ∣phat−M1M∣≤ε0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{M} \mathrel{\htmlData{mx=10}{\implies}} \htmlData{mx=7}{\left\lvert \htmlData{mx=6}{\htmlData{mx=2}{\mathit{phat}} - \htmlData{mx=5}{\frac{\htmlData{mx=3}{M_{1}}}{\htmlData{mx=4}{M}}}} \right\rvert} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\varepsilon}, then

M1≤(1+2ε)⋅(max⁡(0,min⁡(1,phat))+ε1+2ε)⋅M∧M0≤(1+2ε)⋅(1−max⁡(0,min⁡(1,phat))+ε1+2ε)⋅M\begin{aligned} & \htmlData{mx=2}{M_{1}} \\ & \quad \htmlData{mx=1}{\leq} \htmlData{mx=17}{\htmlData{mx=15}{(\htmlData{mx=5}{1 + \htmlData{mx=4}{2\htmlData{mx=3}{\varepsilon}}}) \cdot \left(\htmlData{mx=14}{\frac{\htmlData{mx=10}{\htmlData{mx=8}{\max(0, \htmlData{mx=7}{\min(1, \htmlData{mx=6}{\mathit{phat}})})} + \htmlData{mx=9}{\varepsilon}}}{\htmlData{mx=13}{1 + \htmlData{mx=12}{2\htmlData{mx=11}{\varepsilon}}}}}\right)} \cdot \htmlData{mx=16}{M}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=19}{M_{0}} \\ & \quad \htmlData{mx=18}{\leq} \htmlData{mx=35}{\htmlData{mx=33}{(\htmlData{mx=22}{1 + \htmlData{mx=21}{2\htmlData{mx=20}{\varepsilon}}}) \cdot \left(\htmlData{mx=32}{\frac{\htmlData{mx=28}{\htmlData{mx=26}{1 - \htmlData{mx=25}{\max(0, \htmlData{mx=24}{\min(1, \htmlData{mx=23}{\mathit{phat}})})}} + \htmlData{mx=27}{\varepsilon}}}{\htmlData{mx=31}{1 + \htmlData{mx=30}{2\htmlData{mx=29}{\varepsilon}}}}}\right)} \cdot \htmlData{mx=34}{M}} \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
M, M1, M0, phat, ε range over real numbers: the statement must hold for every choice. ((M M1 M0 phat ε : ℝ))
≤At most
0 is less than or equal to M1. (0 ≤ M1)
+Addition
M1 plus M0. (M1 + M0)
=Equality
M1 + M0 and M are the same. (M1 + M0 = M)
<Less than
0 is strictly smaller than ε. (0 < ε)
⟹Implies
If 0 < M, then |phat − M1/M| ≤ ε. (Between types, A → B is the type of functions from A to B.) (0 < M → |phat - M1 / M| ≤ ε)
∧And
Both hold: M1 ≤ (1 + 2 · ε) · ((max(0, min(1, phat)) + ε)/(1 + 2 · ε)…, and M0 ≤ (1 + 2 · ε) · ((1 − max(0, min(1, phat)) + ε)/(1 + 2 …. (M1 ≤ (1 + 2 * ε) * ((max 0 (min 1 phat)…)
|x|Absolute value
The size of phat − M1/M without its sign. (|phat - M1 / M|)
-Subtraction
phat minus M1/M. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (phat - M1 / M)
·Multiplication
2 times ε. (2 * ε)
a/bDivision
M1 divided by M. In Lean, dividing by 0 gives 0. (M1 / M)
maxMaximum
The larger of 0 and min(1, phat). (max 0 (min 1 phat))
minMinimum
The smaller of 1 and phat. (min 1 phat)

The per-node step of the Conversion Theorem in mass form (cv-smoothed-branch-ratio scaled by the parent mass, with the degenerate M = 0 node handled): every level of the descent under-proposes by at most 1 + 2ε, which is exactly the hypothesis of cv-end-to-end-abstract. Part of 'The Proposal Principle: attention complexity is proposal complexity'.

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
43 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements