Proveddrift-lawdecodeheadline-theoremsingle-statement
Drift Law, one statement: norm-tier certificate |t−s| ≤ ‖q_t−q_s‖κ off O; exact envelope sampling, draws ≤ e^{2δκ}; stratified IS factor ≤ cosh²(δκ); tree reads ≤ (D+1)(1+Ne^{2δκ})+|O|
For all , , , , , , , , and , if , , , , , , , , , , and (given , and ), then
What the notation means · or point at any symbol
- Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to J. Lean writes f x; papers write f(x). (
Fintype J) - Nonempty
- Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Nonempty) - DecidableEq
- DecidableEq: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
DecidableEq) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x : TVariables
- qs, qt range over Fin d → ℝ: the statement must hold for every choice. (
(qs qt : Fin d → ℝ)) - Finset
- Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset) - x ∈ TVariables
- κ, δ range over real numbers: the statement must hold for every choice. (
(κ δ : ℝ)) - ≤At most
- 0 is less than or equal to κ. (
0 ≤ κ) - ∀For all
- The statement after the comma holds for every j. (
∀ j, j ∉ O → ∑ i, k j i ^ 2 ≤ κ ^ 2) - =Equality
- δ and √(∑ i, (qt(i) − qs(i))^2) are the same. (
δ = Real.sqrt (∑ i, (qt i - qs i) ^ 2)) - ∃There exists
- At least one j makes the statement after the comma true. (
∃ j, j ∉ O) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - ⟹Implies
- If Fin(d), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin d → ℝ) - √Square root
- The non-negative number whose square is ∑ i, (qt(i) − qs(i))^2. (
Real.sqrt (∑ i, (qt i - qs i) ^ 2)) - ∉Not an element of
- j is not a member of O. (
j ∉ O) - a/bDivision
- m(j) divided by M. In Lean, dividing by 0 gives 0. (
m j / M) - { a if c; b otherwiseCases (if … then … else)
- exp(t(j)) when j ∈ O, and exp(δ · κ) · exp(s(j)) otherwise. (
if j ∈ O then Real.exp (t j) else Real.…) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ∑Summation
- Add up k(j, i)^2 for every i. (
∑ i, k j i ^ 2) - ∈Element of
- j is a member of O. (
j ∈ O) - |x|Absolute value
- The size of t(j) − s(j) without its sign. (
|t j - s j|) - ·Multiplication
- qs(i) times k(j, i). (
qs i * k j i) - aᵇPower
- k(j, i) raised to the power 2. (
k j i ^ 2) - -Subtraction
- qt(i) minus qs(i). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
qt i - qs i) - eˣExponential function
- e raised to the power t(j), where e ≈ 2.718. (
Real.exp (t j)) - <Less than
- 0 is strictly smaller than m(j). (
0 < m j) - ∧And
- Both hold: 0 < m(j), and exp(t(j)) ≤ m(j). (
0 < m j ∧ Real.exp (t j) ≤ m j) - ∑'Infinite sum
- Add up (n + 1) · p · (1 − p)^n for every n in ℕ. (
∑' n : ℕ, ((n : ℝ) + 1) * p * (1 - p) ^…) - (x : T)As real numbers
- n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(n : ℝ)) - +Addition
- n plus 1. (
(n : ℝ) + 1) - filter
- Finset.univ.filter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset.univ.filter) - x ↦ f(x)Function (λ-abstraction)
- The function sending j to j ∉ O. Lean writes fun x => …; papers write x ↦ …. (
fun j => j ∉ O) - coshHyperbolic cosine
- (eˣ + e⁻ˣ)/2 at δ · κ. (
Real.cosh (δ * κ)) - card
- O.card: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
O.card)
theorem drift-law-provable-form {J : Type} [Fintype J] [Nonempty J] [DecidableEq J] {d : ℕ} (k : J → Fin d → ℝ) (qs qt : Fin d → ℝ) (O : Finset J) (κ δ : ℝ) (hκ0 : 0 ≤ κ) (hκ : ∀ j, j ∉ O → ∑ i, k j i ^ 2 ≤ κ ^ 2) (hδ : δ = Real.sqrt (∑ i, (qt i - qs i) ^ 2)) (s t : J → ℝ) (hs : ∀ j, s j = ∑ i, qs i * k j i) (ht : ∀ j, t j = ∑ i, qt i * k j i) (m : J → ℝ) (hm : ∀ j, m j = if j ∈ O then Real.exp (t j) else Real.exp (δ * κ) * Real.exp (s j)) (M Zt p : ℝ) (hM : M = ∑ j, m j) (hZt : Zt = ∑ j, Real.exp (t j)) (hp : p = ∑ j, (m j / M) * (Real.exp (t j) / m j)) (N D : ℝ) (hN : 0 ≤ N) (hD : 0 ≤ D) (hne : ∃ j, j ∉ O) :
((∀ j, j ∉ O → |t j - s j| ≤ δ * κ) ∧ (∀ j, 0 < m j ∧ Real.exp (t j) ≤ m j) ∧ p = Zt / M ∧ (∀ j, (m j / M) * (Real.exp (t j) / m j) / p = Real.exp (t j) / Zt) ∧ (∑' n : ℕ, ((n : ℝ) + 1) * p * (1 - p) ^ n = M / Zt) ∧ M / Zt ≤ Real.exp (2 * δ * κ)) ∧ ((∑ j ∈ Finset.univ.filter (fun j => j ∉ O), Real.exp (2 * t j - s j)) * (∑ j ∈ Finset.univ.filter (fun j => j ∉ O), Real.exp (s j)) ≤ Real.cosh (δ * κ) ^ 2 * (∑ j ∈ Finset.univ.filter (fun j => j ∉ O), Real.exp (t j)) ^ 2) ∧ ((D + 1) + N * (M / Zt) * (D + 1) + (O.card : ℝ) ≤ (D + 1) * (1 + N * Real.exp (2 * δ * κ)) + (O.card : ℝ))The strongest provable single statement of the Drift Law for decode reuse. Keys k_j, snapshot query q_s, current query q_t, δ = ‖q_t − q_s‖, exceptional set O containing every key of norm > κ. Then: (i) every key outside O drifts by at most δκ in score; (ii) the envelope m = e^{t} on O and e^{δκ}e^{s} off O dominates the current weights, rejection from m/M accepts with probability Z_t/M, accepted keys follow the current row exactly, the expected draws per accepted sample are M/Z_t (geometric series) and M/Z_t ≤ e^{2δκ}; (iii) importance sampling from the stale snapshot on the complement of O has second-moment factor (Σ_{∉O} e^{2t−s})(Σ_{∉O} e^{s}) ≤ cosh²(δκ)(Σ_{∉O} e^{t})²; (iv) for N samples from a depth-D sum-tree with one insertion per token, expected tree reads (D+1) + N(M/Z_t)(D+1) + |O| ≤ (D+1)(1 + N e^{2δκ}) + |O|, independent of the context length apart from D and |O|. Read-count model only: tree construction, path reweighting for O, key/value vector reads and the refresh schedule are charged in prose, not here. Conjoins drift-norm-tiered-exact-decode and drift-stratified-oscillation-bound.
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
- 172 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.