Provedquery-cover-lawdecode-attentionsoftmaxkv-cache
Valid acceptance probabilities and acceptance rate ≥ e^{−2η} when |s_t − s₀| ≤ η (M = η)
For all , and , if and , 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) - ∀For all
- The statement after the comma holds for every j. (
∀ j, |st j - s0 j| ≤ η) - ∧And
- Both hold: ∀ j, exp(st(j) − s0(j) − η) ≤ 1, and exp(−2 · η) ≤ (∑ i, exp(s0(i))/(∑ k, exp(s0(k))) · exp(st(…. (
(∀ j, Real.exp (st j - s0 j - η) ≤ 1) ∧…) - |x|Absolute value
- The size of st(j) − s0(j) without its sign. (
|st j - s0 j|) - ≤At most
- |st(j) − s0(j)| is less than or equal to η. (
|st j - s0 j| ≤ η) - -Subtraction
- st(j) minus s0(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
st j - s0 j) - eˣExponential function
- e raised to the power st(j) − s0(j) − η, where e ≈ 2.718. (
Real.exp (st j - s0 j - η)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - −xNegation
- The negative of 2. (
-2) - ·Multiplication
- −2 times η. (
-2 * η) - a/bDivision
- exp(s0(i)) divided by ∑ k, exp(s0(k)). In Lean, dividing by 0 gives 0. (
Real.exp (s0 i) / ∑ k, Real.exp (s0 k)) - ∑Summation
- Add up exp(s0(k)) for every k. (
∑ k, Real.exp (s0 k))
theorem qc-acceptance-rate {n : ℕ} (s0 st : Fin n → ℝ) (η : ℝ) (hn : 0 < n) (hη : ∀ j, |st j - s0 j| ≤ η) :
(∀ j, Real.exp (st j - s0 j - η) ≤ 1) ∧ Real.exp (-2 * η) ≤ ∑ i, (Real.exp (s0 i) / ∑ k, Real.exp (s0 k)) * Real.exp (st i - s0 i - η)Each acceptance probability e^{s_t−s₀−η} ≤ 1, and the overall acceptance rate Σ π₀(j) e^{s_t(j)−s₀(j)−η} ≥ e^{−2η}. The cost per exact sample depends only on the tilt η, not on the context length n. 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
- 23 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.