proofs
Proveddrift-lawdecodeheadline-theoremsnapshot-reuse

Persistent-snapshot cost theorem: exact snapshot rejection under tilt η accepts at rate in [e^{−2η},1], samples the current row exactly, and N samples cost ≤ N·D·e^{2η} reads

For all J∈Type⁡\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}, s,t:J→R\htmlData{mx=3}{s, t : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}} and η,N,D,Zs,Zt,p∈R\htmlData{mx=1}{\eta, N, D, \mathit{Zs}, \mathit{Zt}, p \in \htmlData{mx=0}{\mathbb{R}}}, if ∀j, ∣t(j)−s(j)∣≤η\htmlData{mx=10}{\forall j,\ \htmlData{mx=7}{\left\lvert \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{t}(\htmlData{mx=1}{j})} - \htmlData{mx=5}{\htmlData{mx=3}{s}(\htmlData{mx=4}{j})}} \right\rvert} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\eta}}, 0≤N0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{N}, 0≤D0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{D}, Zs=∑kes(k)\htmlData{mx=0}{\mathit{Zs}} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\sum_{k} \htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{s}(\htmlData{mx=2}{k})}}}}, Zt=∑ket(k)\htmlData{mx=0}{\mathit{Zt}} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\sum_{k} \htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{t}(\htmlData{mx=2}{k})}}}} and p=∑jes(j)Zs⋅et(j)−s(j)−η\htmlData{mx=0}{p} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\sum_{j} \htmlData{mx=17}{\htmlData{mx=6}{\frac{\htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{s}(\htmlData{mx=2}{j})}}}}{\htmlData{mx=5}{\mathit{Zs}}}} \cdot \htmlData{mx=16}{e^{\htmlData{mx=15}{\htmlData{mx=13}{\htmlData{mx=9}{\htmlData{mx=7}{t}(\htmlData{mx=8}{j})} - \htmlData{mx=12}{\htmlData{mx=10}{s}(\htmlData{mx=11}{j})}} - \htmlData{mx=14}{\eta}}}}}} (given Fintype⁡ J\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}} and Nonempty⁡ J\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}}), then

(∀j, 0<et(j)−s(j)−η∧et(j)−s(j)−η≤1)∧p=e−η⋅ZtZs∧(∀j, es(j)Zs⋅et(j)−s(j)−ηp=et(j)Zt)∧(e−2⋅η≤p∧p≤1)∧(∑k∈N(k+1)⋅p⋅(1−p)k=1p)∧(1p≤e2η)∧(N⋅D⋅(1p)≤N⋅D⋅e2η)\begin{aligned} & (\htmlData{mx=24}{\forall j,\ 0 \mathrel{\htmlData{mx=11}{<}} \htmlData{mx=10}{e^{\htmlData{mx=9}{\htmlData{mx=7}{\htmlData{mx=3}{\htmlData{mx=1}{t}(\htmlData{mx=2}{j})} - \htmlData{mx=6}{\htmlData{mx=4}{s}(\htmlData{mx=5}{j})}} - \htmlData{mx=8}{\eta}}}} \mathbin{\htmlData{mx=23}{\land}} \htmlData{mx=21}{e^{\htmlData{mx=20}{\htmlData{mx=18}{\htmlData{mx=14}{\htmlData{mx=12}{t}(\htmlData{mx=13}{j})} - \htmlData{mx=17}{\htmlData{mx=15}{s}(\htmlData{mx=16}{j})}} - \htmlData{mx=19}{\eta}}}} \mathrel{\htmlData{mx=22}{\leq}} 1}) \\ & \htmlData{mx=0}{\land} \htmlData{mx=25}{p} \mathrel{\htmlData{mx=33}{=}} \htmlData{mx=32}{\frac{\htmlData{mx=30}{\htmlData{mx=28}{e^{\htmlData{mx=27}{-\htmlData{mx=26}{\eta}}}} \cdot \htmlData{mx=29}{\mathit{Zt}}}}{\htmlData{mx=31}{\mathit{Zs}}}} \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=60}{\forall j,\ \htmlData{mx=52}{\frac{\htmlData{mx=50}{\htmlData{mx=39}{\frac{\htmlData{mx=37}{e^{\htmlData{mx=36}{\htmlData{mx=34}{s}(\htmlData{mx=35}{j})}}}}{\htmlData{mx=38}{\mathit{Zs}}}} \cdot \htmlData{mx=49}{e^{\htmlData{mx=48}{\htmlData{mx=46}{\htmlData{mx=42}{\htmlData{mx=40}{t}(\htmlData{mx=41}{j})} - \htmlData{mx=45}{\htmlData{mx=43}{s}(\htmlData{mx=44}{j})}} - \htmlData{mx=47}{\eta}}}}}}{\htmlData{mx=51}{p}}} \mathrel{\htmlData{mx=59}{=}} \htmlData{mx=58}{\frac{\htmlData{mx=56}{e^{\htmlData{mx=55}{\htmlData{mx=53}{t}(\htmlData{mx=54}{j})}}}}{\htmlData{mx=57}{\mathit{Zt}}}}}\right) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=64}{e^{\htmlData{mx=63}{\htmlData{mx=61}{-2} \cdot \htmlData{mx=62}{\eta}}}} \mathrel{\htmlData{mx=66}{\leq}} \htmlData{mx=65}{p} \mathbin{\htmlData{mx=69}{\land}} \htmlData{mx=67}{p} \mathrel{\htmlData{mx=68}{\leq}} 1) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=81}{\sum_{k \in \htmlData{mx=70}{\mathbb{N}}} \htmlData{mx=80}{\htmlData{mx=75}{(\htmlData{mx=73}{\htmlData{mx=72}{\htmlData{mx=71}{k}} + 1}) \cdot \htmlData{mx=74}{p}} \cdot \htmlData{mx=79}{(\htmlData{mx=77}{1 - \htmlData{mx=76}{p}})^{\htmlData{mx=78}{k}}}}} \mathrel{\htmlData{mx=84}{=}} \htmlData{mx=83}{\frac{1}{\htmlData{mx=82}{p}}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=86}{\frac{1}{\htmlData{mx=85}{p}}} \mathrel{\htmlData{mx=90}{\leq}} \htmlData{mx=89}{e^{\htmlData{mx=88}{2\htmlData{mx=87}{\eta}}}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=96}{\htmlData{mx=93}{\htmlData{mx=91}{N} \cdot \htmlData{mx=92}{D}} \cdot \left(\htmlData{mx=95}{\frac{1}{\htmlData{mx=94}{p}}}\right)} \mathrel{\htmlData{mx=104}{\leq}} \htmlData{mx=103}{\htmlData{mx=99}{\htmlData{mx=97}{N} \cdot \htmlData{mx=98}{D}} \cdot \htmlData{mx=102}{e^{\htmlData{mx=101}{2\htmlData{mx=100}{\eta}}}}}\right) \end{aligned}
What the notation means · or point at any symbol
Type
Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype
Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application
Fintype applied to J. Lean writes f x; papers write f(x). (Fintype J)
Nonempty
Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
⟹Implies
If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables
s, t range over J → ℝ: the statement must hold for every choice. ((s t : J → ℝ))
x ∈ TVariables
η, N, D, Zs, Zt, p range over real numbers: the statement must hold for every choice. ((η N D 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))
RReal numbers
The real numbers: every point on the number line. (ℝ)
|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)
<Less than
0 is strictly smaller than exp(t(j) − s(j) − η). (0 < Real.exp (t j - s j - η))
∧And
Both hold: 0 < exp(t(j) − s(j) − η), and exp(t(j) − s(j) − η) ≤ 1. (0 < Real.exp (t j - s j - η) ∧ Real.exp…)
·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)
−xNegation
The negative of η. (-η)
∑'Infinite sum
Add up (k + 1) · p · (1 − p)^k for every k in ℕ. (∑' k : ℕ, ((k : ℝ) + 1) * p * (1 - p) ^…)
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
(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 : ℝ))
+Addition
k plus 1. ((k : ℝ) + 1)
aᵇPower
1 − p raised to the power k. ((1 - p) ^ k)

Single-statement form of Drift Law clause 1. For snapshot scores s and current scores t with |t_j − s_j| ≤ η on every key: every acceptance probability e^{t−s−η} lies in (0,1]; the per-draw acceptance rate is exactly e^{−η}Z_t/Z_s and lies in [e^{−2η}, 1]; conditional on acceptance the key is distributed exactly as the current attention row e^{t}/Z_t; the expected number of draws per accepted sample is exactly 1/p (geometric series, proved as a tsum); and with a depth-D sum-tree per draw, N exact samples cost at most N·D·e^{2η} key reads, independent of context length except through D. Part of 'The Drift Law' (closes the goal item 'single-statement persistent-snapshot cost theorem').

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

More proved statements