proofs
Provedproposal-principleattentionunifiedcrux

CONVERSION THEOREM (one statement): an additively ε-accurate branch-mass oracle on the key tree yields a smoothed proposal r that is a distribution with π_b ≤ (1+2ε)^L r_b and Σπ_b²/r_b ≤ (1+2ε)^L

For all L∈N\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}, π:(Fin⁡ L→Bool⁡)→R\htmlData{mx=7}{\pi : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{L}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\operatorname{Bool}}) \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=5}{\mathbb{R}}}, ε∈R\htmlData{mx=1}{\varepsilon \in \htmlData{mx=0}{\mathbb{R}}}, m:N→(Fin⁡ L→Bool⁡)→R\htmlData{mx=9}{m : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=8}{\to}} (\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{L}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\operatorname{Bool}}) \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}, phat:N→(Fin⁡ L→Bool⁡)→R\htmlData{mx=9}{\mathit{phat} : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=8}{\to}} (\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{L}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\operatorname{Bool}}) \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}, pt,Q:N→(Fin⁡ L→Bool⁡)→R\htmlData{mx=9}{\mathit{pt}, Q : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=8}{\to}} (\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{L}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\operatorname{Bool}}) \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}} and hQ∈∀ℓ,b, Q(ℓ,b)={:(ℓ)<Lif hthen⁡({pt(ℓ,b)if b(⟨ℓ,h⟩)1−pt(ℓ,b)otherwise)otherwise else 1\htmlData{mx=30}{\mathit{hQ} \in \htmlData{mx=29}{\htmlData{mx=28}{\forall \ell, b,\ \htmlData{mx=3}{\htmlData{mx=0}{Q}(\htmlData{mx=1}{\ell}, \htmlData{mx=2}{b})} \mathrel{\htmlData{mx=27}{=}} \htmlData{mx=26}{\begin{cases} \htmlData{mx=5}{\mathtt{:}(\htmlData{mx=4}{\ell})} \mathrel{\htmlData{mx=7}{<}} \htmlData{mx=6}{L} & \text{if } \htmlData{mx=8}{h} \\ \htmlData{mx=25}{\htmlData{mx=9}{\operatorname{then}}\left(\htmlData{mx=24}{\begin{cases} \htmlData{mx=13}{\htmlData{mx=10}{\mathit{pt}}(\htmlData{mx=11}{\ell}, \htmlData{mx=12}{b})} & \text{if } \htmlData{mx=18}{\htmlData{mx=14}{b}(\htmlData{mx=17}{\left\langle \htmlData{mx=15}{\ell}, \htmlData{mx=16}{h} \right\rangle})} \\ \htmlData{mx=23}{1 - \htmlData{mx=22}{\htmlData{mx=19}{\mathit{pt}}(\htmlData{mx=20}{\ell}, \htmlData{mx=21}{b})}} & \text{otherwise} \end{cases}}\right)} & \text{otherwise} \end{cases}}}\,\mathtt{else\ 1}}}, if ∀b, 0≤π(b)\htmlData{mx=4}{\forall b,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{b})}}, ∑bπ(b)=1\htmlData{mx=3}{\sum_{b} \htmlData{mx=2}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{b})}} \mathrel{\htmlData{mx=4}{=}} 1, 0<ε0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}, ∀ℓ,b, m(ℓ,b)=∑b′:Fin⁡ L→Bool⁡({π(b′)if (∀i:Fin⁡ L, i<ℓ  ⟹  b′(i)=b(i))0otherwise)\htmlData{mx=31}{\forall \ell, b,\ \htmlData{mx=3}{\htmlData{mx=0}{m}(\htmlData{mx=1}{\ell}, \htmlData{mx=2}{b})} \mathrel{\htmlData{mx=30}{=}} \htmlData{mx=29}{\sum_{b' : \htmlData{mx=6}{\htmlData{mx=4}{\operatorname{Fin}}\,\htmlData{mx=5}{L}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=7}{\operatorname{Bool}}} \left(\htmlData{mx=28}{\begin{cases} \htmlData{mx=11}{\htmlData{mx=9}{\pi}(\htmlData{mx=10}{b'})} & \text{if } (\htmlData{mx=27}{\forall i : \htmlData{mx=26}{\htmlData{mx=24}{\operatorname{Fin}}\,\htmlData{mx=25}{L}},\ \htmlData{mx=13}{\htmlData{mx=12}{i}} \mathrel{\htmlData{mx=15}{<}} \htmlData{mx=14}{\ell} \mathrel{\htmlData{mx=23}{\implies}} \htmlData{mx=18}{\htmlData{mx=16}{b'}(\htmlData{mx=17}{i})} \mathrel{\htmlData{mx=22}{=}} \htmlData{mx=21}{\htmlData{mx=19}{b}(\htmlData{mx=20}{i})}}) \\ 0 & \text{otherwise} \end{cases}}\right)}}, ∀ℓ, b,b′:Fin⁡ L→Bool⁡, (∀i:Fin⁡ L, i<ℓ  ⟹  b(i)=b′(i))  ⟹  phat(ℓ,b)=phat(ℓ,b′)\htmlData{mx=31}{\forall \ell,\ b, b' : \htmlData{mx=28}{\htmlData{mx=26}{\operatorname{Fin}}\,\htmlData{mx=27}{L}} \mathrel{\htmlData{mx=30}{\to}} \htmlData{mx=29}{\operatorname{Bool}},\ (\htmlData{mx=15}{\forall i : \htmlData{mx=14}{\htmlData{mx=12}{\operatorname{Fin}}\,\htmlData{mx=13}{L}},\ \htmlData{mx=1}{\htmlData{mx=0}{i}} \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\ell} \mathrel{\htmlData{mx=11}{\implies}} \htmlData{mx=6}{\htmlData{mx=4}{b}(\htmlData{mx=5}{i})} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=7}{b'}(\htmlData{mx=8}{i})}}) \mathrel{\htmlData{mx=25}{\implies}} \htmlData{mx=19}{\htmlData{mx=16}{\mathit{phat}}(\htmlData{mx=17}{\ell}, \htmlData{mx=18}{b})} \mathrel{\htmlData{mx=24}{=}} \htmlData{mx=23}{\htmlData{mx=20}{\mathit{phat}}(\htmlData{mx=21}{\ell}, \htmlData{mx=22}{b'})}}, ∀ℓ, h:ℓ<L, b, 0<m(ℓ,b)  ⟹  ∣phat(ℓ,b)−m(ℓ+1,update⁡(b,⟨ℓ,h⟩,true⁡))m(ℓ,b)∣≤ε\htmlData{mx=33}{\forall \ell,\ h : \htmlData{mx=30}{\ell} \mathrel{\htmlData{mx=32}{<}} \htmlData{mx=31}{L},\ b,\ 0 \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{\htmlData{mx=0}{m}(\htmlData{mx=1}{\ell}, \htmlData{mx=2}{b})} \mathrel{\htmlData{mx=29}{\implies}} \htmlData{mx=26}{\left\lvert \htmlData{mx=25}{\htmlData{mx=8}{\htmlData{mx=5}{\mathit{phat}}(\htmlData{mx=6}{\ell}, \htmlData{mx=7}{b})} - \htmlData{mx=24}{\frac{\htmlData{mx=19}{\htmlData{mx=9}{m}(\htmlData{mx=11}{\htmlData{mx=10}{\ell} + 1}, \htmlData{mx=18}{\htmlData{mx=12}{\operatorname{update}}(\htmlData{mx=13}{b}, \htmlData{mx=16}{\left\langle \htmlData{mx=14}{\ell}, \htmlData{mx=15}{h} \right\rangle}, \htmlData{mx=17}{\operatorname{true}})})}}{\htmlData{mx=23}{\htmlData{mx=20}{m}(\htmlData{mx=21}{\ell}, \htmlData{mx=22}{b})}}}} \right\rvert} \mathrel{\htmlData{mx=28}{\leq}} \htmlData{mx=27}{\varepsilon}} and ∀ℓ,b, pt(ℓ,b)=max⁡(0,min⁡(1,phat(ℓ,b)))+ε1+2ε\htmlData{mx=17}{\forall \ell, b,\ \htmlData{mx=3}{\htmlData{mx=0}{\mathit{pt}}(\htmlData{mx=1}{\ell}, \htmlData{mx=2}{b})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\frac{\htmlData{mx=11}{\htmlData{mx=9}{\max(0, \htmlData{mx=8}{\min(1, \htmlData{mx=7}{\htmlData{mx=4}{\mathit{phat}}(\htmlData{mx=5}{\ell}, \htmlData{mx=6}{b})})})} + \htmlData{mx=10}{\varepsilon}}}{\htmlData{mx=14}{1 + \htmlData{mx=13}{2\htmlData{mx=12}{\varepsilon}}}}}}, then

(∑b:Fin⁡ L→Bool⁡∏ℓ=0L−1Q(ℓ,b)=1)∧(∀b, π(b)≤(1+2ε)L⋅∏ℓ=0L−1Q(ℓ,b))∧∑b:Fin⁡ L→Bool⁡π(b)2∏ℓ=0L−1Q(ℓ,b)≤(1+2ε)L\begin{aligned} & \left(\htmlData{mx=12}{\sum_{b : \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{L}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\operatorname{Bool}}} \htmlData{mx=11}{\prod_{\ell=0}^{\htmlData{mx=6}{L} - 1} \htmlData{mx=10}{\htmlData{mx=7}{Q}(\htmlData{mx=8}{\ell}, \htmlData{mx=9}{b})}}} \mathrel{\htmlData{mx=13}{=}} 1\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=30}{\forall b,\ \htmlData{mx=16}{\htmlData{mx=14}{\pi}(\htmlData{mx=15}{b})} \mathrel{\htmlData{mx=29}{\leq}} \htmlData{mx=28}{\htmlData{mx=21}{(\htmlData{mx=19}{1 + \htmlData{mx=18}{2\htmlData{mx=17}{\varepsilon}}})^{\htmlData{mx=20}{L}}} \cdot \htmlData{mx=27}{\prod_{\ell=0}^{\htmlData{mx=22}{L} - 1} \htmlData{mx=26}{\htmlData{mx=23}{Q}(\htmlData{mx=24}{\ell}, \htmlData{mx=25}{b})}}}}\right) \\ & \htmlData{mx=0}{\land} \htmlData{mx=47}{\sum_{b : \htmlData{mx=33}{\htmlData{mx=31}{\operatorname{Fin}}\,\htmlData{mx=32}{L}} \mathrel{\htmlData{mx=35}{\to}} \htmlData{mx=34}{\operatorname{Bool}}} \htmlData{mx=46}{\frac{\htmlData{mx=39}{\htmlData{mx=38}{\htmlData{mx=36}{\pi}(\htmlData{mx=37}{b})}^{2}}}{\htmlData{mx=45}{\prod_{\ell=0}^{\htmlData{mx=40}{L} - 1} \htmlData{mx=44}{\htmlData{mx=41}{Q}(\htmlData{mx=42}{\ell}, \htmlData{mx=43}{b})}}}}} \mathrel{\htmlData{mx=53}{\leq}} \htmlData{mx=52}{(\htmlData{mx=50}{1 + \htmlData{mx=49}{2\htmlData{mx=48}{\varepsilon}}})^{\htmlData{mx=51}{L}}} \end{aligned}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
∀For all
The statement after the comma holds for every b. (∀ b, 0 ≤ π b)
∑Summation
Add up π(b) for every b. (∑ b, π b)
=Equality
∑ b, π(b) and 1 are the same. (∑ b, π b = 1)
<Less than
0 is strictly smaller than ε. (0 < ε)
x : TVariables
pt, Q range over ℕ → (Fin L → Bool) → ℝ: the statement must hold for every choice. ((pt Q : ℕ → (Fin L → Bool) → ℝ))
Fin
Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application
Fin applied to L. Lean writes f x; papers write f(x). (Fin L)
⟹Implies
If Fin(L), then Bool. (Between types, A → B is the type of functions from A to B.) (Fin L → Bool)
≤At most
0 is less than or equal to π(b). (0 ≤ π b)
Bool
Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
πPi
The ratio of a circle's circumference to its diameter, ≈ 3.14159. (π)
RReal numbers
The real numbers: every point on the number line. (ℝ)
maxMaximum
The larger of 0 and min(1, phat(ℓ, b)). (max 0 (min 1 (phat ℓ b)))
∏Product
Multiply together Q(ℓ, b) for ℓ = 0, 1, …, L − 1. (∏ ℓ ∈ Finset.range L, Q ℓ b)
minMinimum
The smaller of 1 and phat(ℓ, b). (min 1 (phat ℓ b))
then
then: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (then)
|x|Absolute value
The size of phat(ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b) without its sign. (|phat ℓ b - m (ℓ + 1) (Function.update …)
-Subtraction
phat(ℓ, b) minus m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (phat ℓ b - m (ℓ + 1) (Function.update b…)
{ a if c; b otherwiseCases (if … then … else)
π(b') when ∀ i, i < ℓ → b'(i) = b(i), and 0 otherwise. (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b…)
a/bDivision
m(ℓ + 1, update(b, ⟨ℓ, h⟩, true)) divided by m(ℓ, b). In Lean, dividing by 0 gives 0. (m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ tru…)
+Addition
ℓ plus 1. (ℓ + 1)
(x : T)As natural numbers
i read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((i : ℕ))
update
Function.update: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Function.update)
·Multiplication
2 times ε. (2 * ε)
∧And
Both hold: ∀ b, π(b) ≤ (1 + 2 · ε)^L · (∏ ℓ, Q(ℓ, b)), and (∑ b, π(b)^2/(∏ ℓ, Q(ℓ, b))) ≤ (1 + 2 · ε)^L. ((∀ b, π b ≤ (1 + 2 * ε) ^ L * ∏ ℓ ∈ Fin…)
aᵇPower
1 + 2 · ε raised to the power L. ((1 + 2 * ε) ^ L)
⟨a, b⟩Anonymous constructor
Builds a structure (a pair, a subtype element, …) from ℓ, h. (⟨ℓ, h⟩)
true
true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (true)

The crux half of the Proposal Principle, fully assembled: oracle phat (depends only on the node's prefix; |phat − conditional mass| ≤ ε), pt = (clip phat + ε)/(1+2ε), Q ℓ b = pt or 1−pt by the bit of b, r b = ∏_ℓ Q ℓ b. Inlines cv-end-to-end-abstract, cv-tree-proposal-sums-to-one, cv-node-mass-inheritance and cv-prefix-masses. With L = ⌈log₂ n⌉ and ε = 1/L the χ² factor is ≤ e² (cv-log-depth-constant), so any accuracy-scalable attention algorithm converts into a proposal scheme with polylog loss. Technique: Jerrum–Valiant–Vazirani counting ⇒ sampling, credited. 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
234 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements