Proveddrift-lawdecodesnapshot-reuseattention-compute-law
Refresh law, one statement: per-token K/V traffic ≤ N(1 + (e−1)c) + n/T + N(e−1)c·T for refresh period T with 2cT ≤ 1
For all and , if , , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- n, N, c range over real numbers: the statement must hold for every choice. (
(n N c : ℝ)) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - <Less than
- 0 is strictly smaller than T. (
0 < T) - ≤At most
- 0 is less than or equal to c. (
0 ≤ c) - ·Multiplication
- 2 times c. (
2 * c) - a/bDivision
- n + N · (∑ t, exp(2 · c · (t + 1))) divided by T. In Lean, dividing by 0 gives 0. (
(n + N * ∑ t ∈ Finset.range T, Real.exp…) - ∑Summation
- Add up exp(2 · c · (t + 1)) for t = 0, 1, …, T − 1. (
∑ t ∈ Finset.range T, Real.exp (2 * c *…) - eˣExponential function
- e raised to the power 2 · c · (t + 1), where e ≈ 2.718. (
Real.exp (2 * c * (t + 1))) - +Addition
- t plus 1. (
t + 1) - -Subtraction
- exp(1) minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
Real.exp 1 - 1)
theorem rl-refresh-law-assembled (n N c : ℝ) (T : ℕ) (hT : 0 < T) (hc : 0 ≤ c) (hN : 0 ≤ N) (hdrift : 2 * c * T ≤ 1) :
(n + N * ∑ t ∈ Finset.range T, Real.exp (2 * c * (t + 1))) / T ≤ N * (1 + (Real.exp 1 - 1) * c) + (n / T + N * (Real.exp 1 - 1) * c * T)Assembled bound for exact snapshot reuse under linear drift c. Loop 2 of the Drift Law shows the drift budget 2cT ≤ 1 caps T at 1/(2c), so the √n optimum is only a transient regime (n ≲ N/(4(e−1)c)); the asymptotic static-refresh traffic is Θ(c n / log n), and only the bounded-drift persistent snapshot is flat in n. Part of 'The Drift Law: decode K/V traffic is set by how far the query drifts' (exact snapshot reuse at decode).
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
Sign in to see the proofThe proof, its signed report and its history.