Provedquery-cover-lawdecode-attentionsoftmaxkv-cache

Greedy snapshots are near-optimal: centres pairwise > η apart number at most the size of ANY cover at radius η/2

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=5}{\mathit{dist} : \htmlData{mx=0}{\alpha} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\alpha} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}$ , $\htmlData{mx=3}{C, B \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=1}{\alpha}}}$ and $\htmlData{mx=1}{\eta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=9}{\forall x, y,\ \htmlData{mx=3}{\htmlData{mx=0}{\mathit{dist}}(\htmlData{mx=1}{x}, \htmlData{mx=2}{y})} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{\htmlData{mx=4}{\mathit{dist}}(\htmlData{mx=5}{y}, \htmlData{mx=6}{x})}}$ , $\htmlData{mx=14}{\forall x, y, z,\ \htmlData{mx=3}{\htmlData{mx=0}{\mathit{dist}}(\htmlData{mx=1}{x}, \htmlData{mx=2}{z})} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\htmlData{mx=7}{\htmlData{mx=4}{\mathit{dist}}(\htmlData{mx=5}{x}, \htmlData{mx=6}{y})} + \htmlData{mx=11}{\htmlData{mx=8}{\mathit{dist}}(\htmlData{mx=9}{y}, \htmlData{mx=10}{z})}}}$ , $\htmlData{mx=13}{\forall x \in \htmlData{mx=12}{C},\ \htmlData{mx=11}{\forall y \in \htmlData{mx=10}{C},\ \htmlData{mx=0}{x} \mathrel{\htmlData{mx=2}{\neq}} \htmlData{mx=1}{y} \mathrel{\htmlData{mx=9}{\implies}} \htmlData{mx=3}{\eta} \mathrel{\htmlData{mx=8}{<}} \htmlData{mx=7}{\htmlData{mx=4}{\mathit{dist}}(\htmlData{mx=5}{x}, \htmlData{mx=6}{y})}}}$ and $\htmlData{mx=10}{\forall x \in \htmlData{mx=9}{C},\ \htmlData{mx=8}{\exists b \in \htmlData{mx=7}{B},\ \htmlData{mx=3}{\htmlData{mx=0}{\mathit{dist}}(\htmlData{mx=1}{x}, \htmlData{mx=2}{b})} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{\frac{\htmlData{mx=4}{\eta}}{2}}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidableEq}}\,\htmlData{mx=1}{\alpha}}$ ), then

\htmlData{mx=0}{\operatorname{card}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\operatorname{card}}

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)
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)
f(x)Function application: DecidableEq applied to α. Lean writes f x; papers write f(x). (DecidableEq α)
∀For all: The statement after the comma holds for every x, y. (∀ x y, dist x y = dist y x)
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: C, B range over Finset α: the statement must hold for every choice. ((C B : Finset α))
card: C.card: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (C.card)
⟹Implies: If α, then ℝ. (Between types, A → B is the type of functions from A to B.) (α → ℝ)
=Equality: dist(x, y) and dist(y, x) are the same. (dist x y = dist y x)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: dist(x, z) is less than or equal to dist(x, y) + dist(y, z). (dist x z ≤ dist x y + dist y z)
∃There exists: At least one b makes the statement after the comma true. (∃ b ∈ B, dist x b ≤ η / 2)
≠Not equal: x and y are different. (x ≠ y)
+Addition: dist(x, y) plus dist(y, z). (dist x y + dist y z)
<Less than: η is strictly smaller than dist(x, y). (η < dist x y)
a/bDivision: η divided by 2. In Lean, dividing by 0 gives 0. (η / 2)

theorem qc-greedy-cover-le-cover {α : Type} [DecidableEq α] (dist : α → α → ℝ) (hsymm : ∀ x y, dist x y = dist y x) (htri : ∀ x y z, dist x z ≤ dist x y + dist y z) (C B : Finset α) (η : ℝ) (hsep : ∀ x ∈ C, ∀ y ∈ C, x ≠ y → η < dist x y) (hcov : ∀ x ∈ C, ∃ b ∈ B, dist x b ≤ η / 2) :
    C.card ≤ B.card

For any distance satisfying symmetry and the triangle inequality (e.g. the key-dual norm max_j |⟨u, k_j⟩|): no radius-η/2 ball holds two η-separated centres, so the greedy online snapshot count at radius η is ≤ the optimal covering number at radius η/2. The Query-Cover Law's N_η is therefore robust to the choice of online versus offline cover. 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: 20 lines of Lean

Greedy snapshots are near-optimal: centres pairwise > η apart number at most the size of ANY cover at radius η/2

How it was proved

More proved statements