Provedquery-cover-lawdecode-attentionsoftmaxkv-cache

Score drift is controlled by query displacement: (⟨q',k⟩ − ⟨q,k⟩)² ≤ ‖q' − q‖² ‖k‖²

For all $\htmlData{mx=1}{d \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=5}{q, q', k : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{d}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ :

\begin{aligned} & \htmlData{mx=18}{\left(\htmlData{mx=17}{\htmlData{mx=8}{\sum_{i} \htmlData{mx=7}{\htmlData{mx=3}{\htmlData{mx=1}{q'}(\htmlData{mx=2}{i})} \cdot \htmlData{mx=6}{\htmlData{mx=4}{k}(\htmlData{mx=5}{i})}}} - \htmlData{mx=16}{\sum_{i} \htmlData{mx=15}{\htmlData{mx=11}{\htmlData{mx=9}{q}(\htmlData{mx=10}{i})} \cdot \htmlData{mx=14}{\htmlData{mx=12}{k}(\htmlData{mx=13}{i})}}}}\right)^{2}} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=33}{\left(\htmlData{mx=27}{\sum_{i} \htmlData{mx=26}{(\htmlData{mx=25}{\htmlData{mx=21}{\htmlData{mx=19}{q'}(\htmlData{mx=20}{i})} - \htmlData{mx=24}{\htmlData{mx=22}{q}(\htmlData{mx=23}{i})}})^{2}}}\right) \cdot \left(\htmlData{mx=32}{\sum_{i} \htmlData{mx=31}{\htmlData{mx=30}{\htmlData{mx=28}{k}(\htmlData{mx=29}{i})}^{2}}}\right)} \end{aligned}

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 d. Lean writes f x; papers write f(x). (Fin d)
⟹Implies: If Fin(d), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin d → ℝ)
x : TVariables: q, q', k range over Fin d → ℝ: the statement must hold for every choice. ((q q' k : Fin d → ℝ))
aᵇPower: (∑ i, q'(i) · k(i)) − (∑ i, q(i) · k(i)) raised to the power 2. ((∑ i, q' i * k i - ∑ i, q i * k i) ^ 2)
≤At most: ((∑ i, q'(i) · k(i)) − (∑ i, q(i) · k(i)))^2 is less than or equal to (∑ i, (q'(i) − q(i))^2) · (∑ i, k(i)^2). ((∑ i, q' i * k i - ∑ i, q i * k i) ^ 2 …)
∑Summation: Add up q'(i) · k(i) for every i. (∑ i, q' i * k i)
-Subtraction: ∑ i, q'(i) · k(i) minus ∑ i, q(i) · k(i). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (∑ i, q' i * k i - ∑ i, q i * k i)
·Multiplication: q'(i) times k(i). (q' i * k i)
RReal numbers: The real numbers: every point on the number line. (ℝ)

theorem qc-score-drift-bound {d : ℕ} (q q' k : Fin d → ℝ) :
    (∑ i, q' i * k i - ∑ i, q i * k i) ^ 2 ≤ (∑ i, (q' i - q i) ^ 2) * (∑ i, k i ^ 2)

Cauchy–Schwarz; gives the cheap sufficient snapshot test ‖q_t − q_s‖·K ≤ η. The exact tilt is the key-dual norm max_j |⟨q_t − q_s, k_j⟩|. 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: 13 lines of Lean

Score drift is controlled by query displacement: (⟨q',k⟩ − ⟨q,k⟩)² ≤ ‖q' − q‖² ‖k‖²

How it was proved

More proved statements