Persistent-snapshot traffic (read-count model): sum-tree descent is exact, insertion touches one node per level, and expected reads per token ≤ (D+1) + N·e^{2η}·(D+1) + |overflow|
For all , , , , , and , if , , , , , and , then
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 < w b) - x ∈ TVariables
- p, η, N, O range over real numbers: the statement must hold for every choice. (
(p η N O : ℝ)) - eˣExponential function
- e raised to the power −2 · η, where e ≈ 2.718. (
Real.exp (-2 * η)) - ≤At most
- exp(−2 · η) is less than or equal to p. (
Real.exp (-2 * η) ≤ p) - 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 D. Lean writes f x; papers write f(x). (
Fin D) - ⟹Implies
- If Fin(D), then Bool. (Between types, A → B is the type of functions from A to B.) (
Fin D → Bool) - <Less than
- 0 is strictly smaller than w(b). (
0 < w b) - ∏Product
- Multiply together M(ℓ + 1, b)/M(ℓ, b) for ℓ = 0, 1, …, D − 1. (
∏ ℓ ∈ Finset.range D, (M (ℓ + 1) b / M …) - 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) - −xNegation
- The negative of 2. (
-2) - ·Multiplication
- −2 times η. (
-2 * η) - ∑Summation
- Add up w(b') if ∀ i, i < ℓ → b'(i) = b(i), else 0 for every b' in Fin(D) → Bool. (
∑ b' : Fin D → Bool, (if (∀ i : Fin D, …) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - a/bDivision
- M(ℓ + 1, b) divided by M(ℓ, b). In Lean, dividing by 0 gives 0. (
M (ℓ + 1) b / M ℓ b) - { a if c; b otherwiseCases (if … then … else)
- w(b') when ∀ i, i < ℓ → b'(i) = b(i), and 0 otherwise. (
if (∀ i : Fin D, (i : ℕ) < ℓ → b' i = b…) - (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 : ℕ)) - =Equality
- b'(i) and b(i) are the same. (
b' i = b i) - -Subtraction
- M'(ℓ, b) minus M(ℓ, b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
M' ℓ b - M ℓ b) - +Addition
- w(b') plus δ if b' = b₀, else 0. (
w b' + if b' = b₀ then δ else 0) - ∧And
- Both hold: (∑' k, (k + 1) · p · (1 − p)^k) = 1/p, and D + 1 + N · (1/p) · (D + 1) + O ≤ D + 1 + N · exp(2 · η) ·…. (
(∑' k : ℕ, ((k : ℝ) + 1) * p * (1 - p) …) - ∑'Infinite sum
- Add up (k + 1) · p · (1 − p)^k for every k in ℕ. (
∑' k : ℕ, ((k : ℝ) + 1) * p * (1 - p) ^…) - (x : T)As real numbers
- k read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(k : ℝ)) - aᵇPower
- 1 − p raised to the power k. (
(1 - p) ^ k)
theorem drift-persistent-snapshot-traffic {D : ℕ} (w : (Fin D → Bool) → ℝ) (hw : ∀ b, 0 < w b) (M : ℕ → (Fin D → Bool) → ℝ) (hM : ∀ ℓ b, M ℓ b = ∑ b' : Fin D → Bool, (if (∀ i : Fin D, (i : ℕ) < ℓ → b' i = b i) then w b' else 0)) (b₀ : Fin D → Bool) (δ : ℝ) (M' : ℕ → (Fin D → Bool) → ℝ) (hM' : ∀ ℓ b, M' ℓ b = ∑ b' : Fin D → Bool, (if (∀ i : Fin D, (i : ℕ) < ℓ → b' i = b i) then (w b' + if b' = b₀ then δ else 0) else 0)) (p η N O : ℝ) (hp : Real.exp (-2 * η) ≤ p) (hp1 : p ≤ 1) (hN : 0 ≤ N) (hO : 0 ≤ O) :
(∀ b, ∏ ℓ ∈ Finset.range D, (M (ℓ + 1) b / M ℓ b) = w b / ∑ b', w b') ∧ (∀ ℓ b, M' ℓ b - M ℓ b = if (∀ i : Fin D, (i : ℕ) < ℓ → b₀ i = b i) then δ else 0) ∧ (∑' k : ℕ, ((k : ℝ) + 1) * p * (1 - p) ^ k = 1 / p) ∧ ((D + 1 : ℝ) + N * (1 / p) * (D + 1) + O ≤ (D + 1 : ℝ) + N * Real.exp (2 * η) * (D + 1) + O)Answers the round-1/3 objection (codex) that no persistent-snapshot cost or traffic law was proven, within an explicit read-count model. Keys are the 2^D leaves of a sum-tree whose node at level ℓ stores the prefix mass M(ℓ, b) of snapshot weights w > 0. (1) Exactness: descending by child/parent mass ratios reaches each key with probability exactly w(b)/Σw (telescoping). (2) Locality: appending weight δ to key b₀ changes M(ℓ, b) by δ exactly on b₀'s path and by 0 elsewhere, so an insertion writes D+1 nodes. (3) Draws: the expected number of draws per accepted rejection sample is exactly 1/p (geometric series), and with acceptance p ≥ e^{−2η} the expected reads per token (one insertion, N samples each costing a D-node descent plus one key read per draw, plus |overflow| keys read exactly) are at most (D+1) + N·e^{2η}·(D+1) + |overflow|, against n reads for exact decode. Scope: a read-count model, not wall-clock; overflow and acceptance as hypotheses (acceptance proven in drift-persistent-snapshot-cost, overflow by the box/residual certificate).
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
- 84 lines of Lean