Proveddrift-lawdecodesum-treeexactness
Sum-tree insertion: adding weight w to a leaf and to every ancestor preserves parent = left + right at every node
For all , if , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- parent, left, right, w range over real numbers: the statement must hold for every choice. (
(parent left right w : ℝ)) - =Equality
- parent and left + right are the same. (
parent = left + right) - ∧And
- Both hold: parent + w = left + w + right, and parent + w = left + (right + w). (
parent + w = (left + w) + right ∧ paren…) - +Addition
- left plus right. (
left + right)
theorem st-sumtree-insert-preserves (parent left right w : ℝ) (h : parent = left + right) :
parent + w = (left + w) + right ∧ parent + w = left + (right + w)Appending a key (scored once against the snapshot query) is an O(log n) update that keeps every node's mass equal to the sum of its children, so the snapshot stays exact as the context grows. 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
- 10 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.