Proveddrift-lawdecodesnapshot-reuseattention-compute-law
Per-token traffic with refresh: (n + N S)/T ≤ n/T + N(1 + (e−1)c(T+1)) given the window bound S
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 N. (
0 ≤ N) - a/bDivision
- n + N · S divided by T. In Lean, dividing by 0 gives 0. (
(n + N * S) / T) - ·Multiplication
- exp(1) − 1 times c. (
(Real.exp 1 - 1) * c) - eˣExponential function
- e raised to the power 1, where e ≈ 2.718. (
Real.exp 1) - -Subtraction
- exp(1) minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
Real.exp 1 - 1) - +Addition
- T plus 1. (
T + 1)
theorem rl-per-token-traffic (n N c : ℝ) (T : ℕ) (hT : 0 < T) (hN : 0 ≤ N) (S : ℝ) (hS : S ≤ T + (Real.exp 1 - 1) * c * (T * (T + 1))) :
(n + N * S) / T ≤ n / T + N * (1 + (Real.exp 1 - 1) * c * (T + 1))Combines the refresh pass and N rejection draws per token into a per-token K/V traffic bound. 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
- 16 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.