Drift Law lower bound (snapshot model): uniform snapshot, m of n keys drifting by x = e^{ct}: reuse cost = n(mx²+n−m)/(mx+n−m)² ≥ (m/4n)·x² until saturation
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. (
ℕ) - Finset
- Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 1 is less than or equal to x. (
1 ≤ x) - <Less than
- 0 is strictly smaller than card. (
0 < S.card) - (x : T)As real numbers
- card read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(S.card : ℝ)) - ·Multiplication
- card times x. (
(S.card : ℝ) * x) - ∧And
- Both hold: (∑ j, (x if j ∈ S, else 1/(∑ k, x if k ∈ S, else 1))^2/(1/…, and card/(4 · n) · x^2 ≤ n · (card · x^2 + (n − card))/(card ·…. (
(∑ j : Fin n, ((if j ∈ S then x else 1)…) - =Equality
- ∑ j, (x if j ∈ S, else 1/(∑ k, x if k ∈ S, else 1))^2/(1/n) and n · (card · x^2 + (n − card))/(card · x + (n − card))^2 are the same. (
∑ j : Fin n, ((if j ∈ S then x else 1) …) - card
- S.card: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
S.card) - 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 n. Lean writes f x; papers write f(x). (
Fin n) - aᵇPower
- x if j ∈ S, else 1/(∑ k, x if k ∈ S, else 1) raised to the power 2. (
((if j ∈ S then x else 1) / ∑ k : Fin n…) - a/bDivision
- x if j ∈ S, else 1 divided by ∑ k, x if k ∈ S, else 1. In Lean, dividing by 0 gives 0. (
(if j ∈ S then x else 1) / ∑ k : Fin n,…) - { a if c; b otherwiseCases (if … then … else)
- x when j ∈ S, and 1 otherwise. (
if j ∈ S then x else 1) - -Subtraction
- n minus card. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
n - S.card) - ∈Element of
- j is a member of S. (
j ∈ S) - ∑Summation
- Add up x if k ∈ S, else 1 for every k in Fin(n). (
∑ k : Fin n, (if k ∈ S then x else 1)) - +Addition
- card · x^2 plus n − card. (
S.card * x ^ 2 + (n - S.card))
theorem drift-snapshot-model-lower-bound {n : ℕ} (S : Finset (Fin n)) (x : ℝ) (hx : 1 ≤ x) (hm : 0 < S.card) (hmn : S.card < n) (hsat : (S.card : ℝ) * x ≤ n - S.card) :
(∑ j : Fin n, ((if j ∈ S then x else 1) / ∑ k : Fin n, (if k ∈ S then x else 1)) ^ 2 / (1 / (n : ℝ)) = n * (S.card * x ^ 2 + (n - S.card)) / (S.card * x + (n - S.card)) ^ 2) ∧ (S.card : ℝ) / (4 * n) * x ^ 2 ≤ n * (S.card * x ^ 2 + (n - S.card)) / (S.card * x + (n - S.card)) ^ 2Explicit instance showing the exponential growth in the Drift Law's upper bound is necessary within the snapshot-reuse model. With a uniform snapshot row over n keys and a set S of m keys whose scores rise by ct (x = e^{ct}), the exact reuse cost factor Σ_j π_t(j)²/π_s(j) equals n(m x² + n − m)/(m x + n − m)², and while m x ≤ n − m it is at least (m/(4n))·x² = (m/(4n))e^{2ct}. Any method that samples the current row by importance or rejection from the stale snapshot therefore pays per-sample cost growing like e^{2ct}, matching the e^{2ct} of drift-persistent-snapshot-cost and rl-refresh-law-assembled in shape; the static-refresh Θ(c·n/log n) clause is tight within this model up to the factor m/(4n). Not a lower bound against all algorithms.
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
- 45 lines of Lean