Provedproposal-principleattentionunifiedcrux

Conversion step: an additive-ε estimate of a branch mass, clipped and smoothed as (p̂_c + ε)/(1 + 2ε), under-proposes neither branch by more than 1 + 2ε

For all $\htmlData{mx=1}{p, \mathit{phat}, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{p}$ , $\htmlData{mx=0}{p} \mathrel{\htmlData{mx=1}{\leq}} 1$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}$ and $\htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{\mathit{phat}} - \htmlData{mx=1}{p}} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\varepsilon}$ , then

\begin{aligned} & \htmlData{mx=1}{p} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{(\htmlData{mx=4}{1 + \htmlData{mx=3}{2\htmlData{mx=2}{\varepsilon}}}) \cdot \left(\htmlData{mx=13}{\frac{\htmlData{mx=9}{\htmlData{mx=7}{\max(0, \htmlData{mx=6}{\min(1, \htmlData{mx=5}{\mathit{phat}})})} + \htmlData{mx=8}{\varepsilon}}}{\htmlData{mx=12}{1 + \htmlData{mx=11}{2\htmlData{mx=10}{\varepsilon}}}}}\right)} \\ & \htmlData{mx=0}{\land} \htmlData{mx=18}{1 - \htmlData{mx=17}{p}} \\ & \quad \htmlData{mx=16}{\leq} \htmlData{mx=32}{(\htmlData{mx=21}{1 + \htmlData{mx=20}{2\htmlData{mx=19}{\varepsilon}}}) \cdot \left(\htmlData{mx=31}{\frac{\htmlData{mx=27}{\htmlData{mx=25}{1 - \htmlData{mx=24}{\max(0, \htmlData{mx=23}{\min(1, \htmlData{mx=22}{\mathit{phat}})})}} + \htmlData{mx=26}{\varepsilon}}}{\htmlData{mx=30}{1 + \htmlData{mx=29}{2\htmlData{mx=28}{\varepsilon}}}}}\right)} \end{aligned}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: p, phat, ε range over real numbers: the statement must hold for every choice. ((p phat ε : ℝ))
≤At most: 0 is less than or equal to p. (0 ≤ p)
<Less than: 0 is strictly smaller than ε. (0 < ε)
|x|Absolute value: The size of phat − p without its sign. (|phat - p|)
∧And: Both hold: p ≤ (1 + 2 · ε) · ((max(0, min(1, phat)) + ε)/(1 + 2 · ε)), and 1 − p ≤ (1 + 2 · ε) · ((1 − max(0, min(1, phat)) + ε)/(1 +…. (p ≤ (1 + 2 * ε) * ((max 0 (min 1 phat) …)
-Subtraction: phat minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (phat - p)
+Addition: 1 plus 2 · ε. (1 + 2 * ε)
·Multiplication: 2 times ε. (2 * ε)
a/bDivision: max(0, min(1, phat)) + ε divided by 1 + 2 · ε. In Lean, dividing by 0 gives 0. ((max 0 (min 1 phat) + ε) / (1 + 2 * ε))
maxMaximum: The larger of 0 and min(1, phat). (max 0 (min 1 phat))
minMinimum: The smaller of 1 and phat. (min 1 phat)

theorem cv-smoothed-branch-ratio (p phat ε : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hε : 0 < ε) (hacc : |phat - p| ≤ ε) :
    p ≤ (1 + 2 * ε) * ((max 0 (min 1 phat) + ε) / (1 + 2 * ε)) ∧ 1 - p ≤ (1 + 2 * ε) * ((1 - max 0 (min 1 phat) + ε) / (1 + 2 * ε))

Conversion Theorem (crux of the Proposal Principle): any attention algorithm that is additively ε-accurate on arbitrary key subsets, queried with indicator values, gives estimated conditional masses down a binary tree of key blocks; smoothing makes each level's likelihood ratio ≤ 1 + 2ε. 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: 25 lines of Lean

Conversion step: an additive-ε estimate of a branch mass, clipped and smoothed as (p̂_c + ε)/(1 + 2ε), under-proposes neither branch by more than 1 + 2ε

How it was proved

More proved statements