Proveddrift-lawdecodesnapshot-reuseattention-compute-law
Diffusive refresh trade-off: n/s² + K s ≥ 3 (n K²/4)^{1/3} (three-term AM–GM)
For all , 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, K, s range over real numbers: the statement must hold for every choice. (
(n K s : ℝ)) - ≤At most
- 0 is less than or equal to n. (
0 ≤ n) - <Less than
- 0 is strictly smaller than s. (
0 < s) - aᵇPower
- n · (K/2) · (K/2) raised to the power 1/3. (
(n * (K / 2) * (K / 2)) ^ ((1 : ℝ) / 3)) - ·Multiplication
- n times K/2. (
n * (K / 2)) - a/bDivision
- K divided by 2. In Lean, dividing by 0 gives 0. (
K / 2) - (x : T)As real numbers
- 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 : ℝ)) - +Addition
- n/s^2 plus K · s. (
n / s ^ 2 + K * s)
theorem rl-diffusive-amgm (n K s : ℝ) (hn : 0 ≤ n) (hK : 0 ≤ K) (hs : 0 < s) :
3 * (n * (K / 2) * (K / 2)) ^ ((1 : ℝ) / 3) ≤ n / s ^ 2 + K * sThe n^{1/3} transient for diffusive drift η_t ∝ √t (substituting T = s²). 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
- 17 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.