Proveddrift-lawdecodesnapshot-reuseattention-compute-law

Refresh trade-off: n/T + K T ≥ 2√(nK) for T > 0

For all $\htmlData{mx=1}{n, K, T \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{n}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{K}$ and $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{T}$ , then

\htmlData{mx=4}{2\htmlData{mx=3}{\sqrt{\htmlData{mx=2}{\htmlData{mx=0}{n} \cdot \htmlData{mx=1}{K}}}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\htmlData{mx=7}{\frac{\htmlData{mx=5}{n}}{\htmlData{mx=6}{T}}} + \htmlData{mx=10}{\htmlData{mx=8}{K} \cdot \htmlData{mx=9}{T}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: n, K, T range over real numbers: the statement must hold for every choice. ((n K T : ℝ))
≤At most: 0 is less than or equal to n. (0 ≤ n)
<Less than: 0 is strictly smaller than T. (0 < T)
√Square root: The non-negative number whose square is n · K. (Real.sqrt (n * K))
·Multiplication: n times K. (n * K)
a/bDivision: n divided by T. In Lean, dividing by 0 gives 0. (n / T)
+Addition: n/T plus K · T. (n / T + K * T)

theorem rl-refresh-amgm (n K T : ℝ) (hn : 0 ≤ n) (hK : 0 ≤ K) (hT : 0 < T) :
    2 * Real.sqrt (n * K) ≤ n / T + K * T

The economic-order-quantity inequality (Harris 1913) for the refresh period: a full pass of n keys every T tokens against drift cost K T. 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: 15 lines of Lean

Refresh trade-off: n/T + K T ≥ 2√(nK) for T > 0

How it was proved

More proved statements