Provedquery-cover-lawdecode-attentionsoftmaxkv-cache
Within a bucket of width w the tilt varies by at most A·w: |a z_j − a z_b| ≤ A w
For all , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- a, zj, zb, A, w range over real numbers: the statement must hold for every choice. (
(a zj zb A w : ℝ)) - |x|Absolute value
- The size of a without its sign. (
|a|) - ≤At most
- |a| is less than or equal to A. (
|a| ≤ A) - -Subtraction
- zj minus zb. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
zj - zb) - ·Multiplication
- a times zj. (
a * zj)
theorem qs-bucket-tilt-bound (a zj zb A w : ℝ) (ha : |a| ≤ A) (hz : |zj - zb| ≤ w) (hw : 0 ≤ w) :
|a * zj - a * zb| ≤ A * wWith w = 1/(2A) the log-ratio is ≤ 1/2 and acceptance ≥ e^{−1}. 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
- 11 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.