Provedquery-cover-lawdecode-attentionsoftmaxkv-cache
Bucket count (z_max − z_min)/(1/(2A)) = 2A(z_max − z_min), independent of n
For all , if , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- A, zmin, zmax range over real numbers: the statement must hold for every choice. (
(A zmin zmax : ℝ)) - <Less than
- 0 is strictly smaller than A. (
0 < A) - =Equality
- (zmax − zmin)/(1/(2 · A)) and 2 · A · (zmax − zmin) are the same. (
(zmax - zmin) / (1 / (2 * A)) = 2 * A *…) - -Subtraction
- zmax minus zmin. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
zmax - zmin) - a/bDivision
- 1 divided by 2 · A. In Lean, dividing by 0 gives 0. (
1 / (2 * A)) - ·Multiplication
- 2 times A. (
2 * A)
theorem qs-bucket-count (A zmin zmax : ℝ) (hA : 0 < A) :
(zmax - zmin) / (1 / (2 * A)) = 2 * A * (zmax - zmin)Per-query cost O(A·Δz + 1/ε) for a rank-1 trajectory whose covering number can be ≈ T. For T ≪ n this beats the Query-Cover Law's n·N/T, refuting its lower bound for low-rank trajectories; the corrected conjecture must involve the trajectory's dimension. 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
- 10 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.