Proveddrift-lawdecodesum-treetraffic
Persistent-snapshot traffic, end-to-end: the sampler's actual acceptance rate p = e^{−η}Z_t/Z_s drives the read bound (D+1) + N·(1/p)·(D+1) + |overflow| ≤ (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. (
ℕ) - x : TVariables
- s, t range over (Fin D → Bool) → ℝ: the statement must hold for every choice. (
(s t : (Fin D → Bool) → ℝ)) - x ∈ TVariables
- η, N, O, Zs, Zt, p, δ range over real numbers: the statement must hold for every choice. (
(η N O Zs Zt p δ : ℝ)) - ∀For all
- The statement after the comma holds for every j. (
∀ j, |t j - s j| ≤ η) - =Equality
- Zs and ∑ k, exp(s(k)) are the same. (
Zs = ∑ k, Real.exp (s k)) - 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) - |x|Absolute value
- The size of t(j) − s(j) without its sign. (
|t j - s j|) - ≤At most
- |t(j) − s(j)| is less than or equal to η. (
|t j - s j| ≤ η) - ∑Summation
- Add up exp(s(k)) for every k. (
∑ k, Real.exp (s k)) - -Subtraction
- t(j) minus s(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
t j - s j) - ∏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) - ·Multiplication
- exp(s(j))/Zs times exp(t(j) − s(j) − η). (
(Real.exp (s j) / Zs) * Real.exp (t j -…) - eˣExponential function
- e raised to the power s(k), where e ≈ 2.718. (
Real.exp (s k)) - a/bDivision
- exp(s(j)) divided by Zs. In Lean, dividing by 0 gives 0. (
Real.exp (s j) / Zs) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - { a if c; b otherwiseCases (if … then … else)
- exp(s(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 : ℕ)) - <Less than
- i is strictly smaller than ℓ. (
(i : ℕ) < ℓ) - +Addition
- exp(s(b')) plus δ if b' = b₀, else 0. (
Real.exp (s b') + if b' = b₀ then δ els…) - −xNegation
- The negative of η. (
-η) - ∧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-end-to-end {D : ℕ} (s t : (Fin D → Bool) → ℝ) (η N O Zs Zt p δ : ℝ) (hη : ∀ j, |t j - s j| ≤ η) (hN : 0 ≤ N) (hO : 0 ≤ O) (hZs : Zs = ∑ k, Real.exp (s k)) (hZt : Zt = ∑ k, Real.exp (t k)) (hp : p = ∑ j, (Real.exp (s j) / Zs) * Real.exp (t j - s j - η)) (M : ℕ → (Fin D → Bool) → ℝ) (hM : ∀ ℓ b, M ℓ b = ∑ b' : Fin D → Bool, (if (∀ i : Fin D, (i : ℕ) < ℓ → b' i = b i) then Real.exp (s 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 (Real.exp (s b') + if b' = b₀ then δ else 0) else 0)) :
(∀ b, ∏ ℓ ∈ Finset.range D, (M (ℓ + 1) b / M ℓ b) = Real.exp (s b) / ∑ b', Real.exp (s b')) ∧ (∀ ℓ b, M' ℓ b - M ℓ b = if (∀ i : Fin D, (i : ℕ) < ℓ → b₀ i = b i) then δ else 0) ∧ (∀ j, (Real.exp (s j) / Zs) * Real.exp (t j - s j - η) / p = Real.exp (t j) / Zt) ∧ p = Real.exp (-η) * Zt / Zs ∧ (∑' 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 review round 6 (codex), which noted that drift-persistent-snapshot-traffic left the acceptance rate p as a free parameter. Here p is defined as the actual per-draw acceptance probability of rejection from the persistent snapshot (snapshot weights e^{s} in a sum-tree over 2^D keys, current scores t, pointwise drift |t − s| ≤ η). One statement: sum-tree descent reaches each key with probability e^{s_b}/Σe^{s}; appending weight δ changes only the D+1 nodes on the new key's path; accepted keys are distributed exactly as the current row e^{t}/Z_t; p = e^{−η}Z_t/Z_s; expected draws per sample = 1/p (geometric series); and the expected reads per token (insertion, N samples at D+1 reads per draw, overflow keys) are at most (D+1) + N·e^{2η}·(D+1) + |overflow|. Embeds drift-persistent-snapshot-cost and drift-persistent-snapshot-traffic. Scope: an explicit read-count model (not wall-clock), estimates are exactly unbiased, not deterministic equality with full softmax.
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
- 158 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.