Proveddrift-lawdecodesnapshot-reuseattention-compute-law
Snapshot window cost under linear drift: Σ_{t=1}^{T} e^{2ct} ≤ T + (e−1)c T(T+1) when 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. (
ℝ) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - ≤At most
- 0 is less than or equal to c. (
0 ≤ c) - ·Multiplication
- 2 times c. (
2 * c) - ∑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-window-cost (c : ℝ) (T : ℕ) (hc : 0 ≤ c) (hT : 2 * c * T ≤ 1) :
∑ t ∈ Finset.range T, Real.exp (2 * c * (t + 1)) ≤ T + (Real.exp 1 - 1) * c * (T * (T + 1))Total rejection draws per unit sample over a refresh window of T tokens when the query drifts by ct in score units. 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
- 33 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.