proofs
Proveddrift-lawdecodesum-treeexactness

Sum-tree branch probabilities are a distribution: left/(left+right) ≥ 0 and the two branch probabilities sum to 1

For all left,right∈R\htmlData{mx=1}{\mathit{left}, \mathit{right} \in \htmlData{mx=0}{\mathbb{R}}}, if 0≤left0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\mathit{left}}, 0≤right0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\mathit{right}} and 0<left+right0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{\mathit{left}} + \htmlData{mx=1}{\mathit{right}}}, then

0≤leftleft+right∧leftleft+right+rightleft+right=1\begin{aligned} & 0 \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{\frac{\htmlData{mx=1}{\mathit{left}}}{\htmlData{mx=4}{\htmlData{mx=2}{\mathit{left}} + \htmlData{mx=3}{\mathit{right}}}}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=17}{\htmlData{mx=11}{\frac{\htmlData{mx=7}{\mathit{left}}}{\htmlData{mx=10}{\htmlData{mx=8}{\mathit{left}} + \htmlData{mx=9}{\mathit{right}}}}} + \htmlData{mx=16}{\frac{\htmlData{mx=12}{\mathit{right}}}{\htmlData{mx=15}{\htmlData{mx=13}{\mathit{left}} + \htmlData{mx=14}{\mathit{right}}}}}} \mathrel{\htmlData{mx=18}{=}} 1 \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
left, right range over real numbers: the statement must hold for every choice. ((left right : ℝ))
≤At most
0 is less than or equal to left. (0 ≤ left)
<Less than
0 is strictly smaller than left + right. (0 < left + right)
∧And
Both hold: 0 ≤ left/(left + right), and left/(left + right) + right/(left + right) = 1. (0 ≤ left / (left + right) ∧ left / (lef…)
+Addition
left plus right. (left + right)
a/bDivision
left divided by left + right. In Lean, dividing by 0 gives 0. (left / (left + right))
=Equality
left/(left + right) + right/(left + right) and 1 are the same. (left / (left + right) + right / (left +…)

Each node's branch choice is a valid two-point distribution whenever the node's mass is positive. Part of 'The Drift Law' (persistent snapshot data structure: the sum-tree that keeps a snapshot sampleable as keys are appended).

How it was proved

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

More proved statements