Provedquery-cover-lawdecode-attentionsoftmaxkv-cache
Rejection from a stale attention snapshot is exact: propose j ~ softmax(s₀), accept w.p. e^{s_t(j)−s₀(j)−M} ⇒ j ~ softmax(s_t) exactly
For all , , and , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - 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) - f(x)Function application
- Fin applied to n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℝ) - x : TVariables
- s0, st range over Fin n → ℝ: the statement must hold for every choice. (
(s0 st : Fin n → ℝ)) - <Less than
- 0 is strictly smaller than n. (
0 < n) - ·Multiplication
- exp(s0(j))/(∑ k, exp(s0(k))) times exp(st(j) − s0(j) − M). (
(Real.exp (s0 j) / ∑ k, Real.exp (s0 k)…) - =Equality
- exp(s0(j))/(∑ k, exp(s0(k))) · exp(st(j) − s0(j) − M)/(∑ i… and exp(st(j))/(∑ k, exp(st(k))) are the same. (
(Real.exp (s0 j) / ∑ k, Real.exp (s0 k)…) - eˣExponential function
- e raised to the power s0(j), where e ≈ 2.718. (
Real.exp (s0 j)) - a/bDivision
- exp(s0(j)) divided by ∑ k, exp(s0(k)). In Lean, dividing by 0 gives 0. (
Real.exp (s0 j) / ∑ k, Real.exp (s0 k)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ∑Summation
- Add up exp(s0(k)) for every k. (
∑ k, Real.exp (s0 k)) - -Subtraction
- st(j) minus s0(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
st j - s0 j)
theorem qc-rejection-from-snapshot-exact {n : ℕ} (s0 st : Fin n → ℝ) (M : ℝ) (j : Fin n) (hn : 0 < n) :
(Real.exp (s0 j) / ∑ k, Real.exp (s0 k)) * Real.exp (st j - s0 j - M) / ∑ i, (Real.exp (s0 i) / ∑ k, Real.exp (s0 k)) * Real.exp (st i - s0 i - M) = Real.exp (st j) / ∑ k, Real.exp (st k)KV-cache keys are fixed during decoding, so the current attention row is an exponential tilt of any stale snapshot. Accepted keys are exact samples from the current row: the estimate is unbiased with variance ≤ F²/N, with no SNIS ratio bias and no MLMC debiasing. Part of 'The Query-Cover Law: decode attention cost is set by where the queries go, not by how long the context is'.
How it was proved
- Proved
- 4 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
- 21 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.