Provedgrouped-query-attentiondecodehead-packingsampleability-law

Exact-head packing attains the bound: placing E exact heads contiguously in groups of G hits exactly ⌈E/G⌉ groups

For all $\htmlData{mx=1}{E, G \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{G}$ , then

\htmlData{mx=20}{\lvert \htmlData{mx=19}{\htmlData{mx=10}{\operatorname{image}}\left(\htmlData{mx=18}{i \mapsto \htmlData{mx=14}{\frac{\htmlData{mx=12}{\htmlData{mx=11}{i}}}{\htmlData{mx=13}{G}}}}\right)} \rvert} \mathrel{\htmlData{mx=27}{=}} \htmlData{mx=26}{\frac{\htmlData{mx=24}{\htmlData{mx=23}{\htmlData{mx=21}{E} + \htmlData{mx=22}{G}} - 1}}{\htmlData{mx=25}{G}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: E, G range over natural numbers: the statement must hold for every choice. ((E G : ℕ))
<Less than: 0 is strictly smaller than G. (0 < G)
|s|Cardinality: The number of elements of image(i ↦ i/G). ((Finset.univ.image (fun i : Fin E => (i…)
=Equality: card(image(i ↦ i/G)) and (E + G − 1)/G are the same. ((Finset.univ.image (fun i : Fin E => (i…)
image: Finset.univ.image: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ.image)
x ↦ f(x)Function (λ-abstraction): The function sending i to i/G. Lean writes fun x => …; papers write x ↦ …. (fun i : Fin E => (i : ℕ) / G)
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 E. Lean writes f x; papers write f(x). (Fin E)
(x : T)As natural numbers: i read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((i : ℕ))
a/bDivision: i divided by G. In Lean, dividing by 0 gives 0. ((i : ℕ) / G)
+Addition: E plus G. (E + G)
-Subtraction: E + G minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (E + G - 1)

theorem pk-packing-attains (E G : ℕ) (hG : 0 < G) :
    (Finset.univ.image (fun i : Fin E => (i : ℕ) / G)).card = (E + G - 1) / G

Grouping query heads by exactness need (rather than adjacency) brings the GQA group-level exact fraction from 1 − (1 − f)^G down to ≈ f within each layer. Prior art groups heads by activation similarity for accuracy (AsymGQA, key-driven GQA, aligned merging); grouping by exactness need for decode traffic was not found. The gain depends on how many exact heads share a layer. Part of 'The Sampleability Law' / 'The Drift Law' (GQA exact-head packing: minimising KV groups that must be read in full).

How it was proved

Proved: 5 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: 34 lines of Lean

Exact-head packing attains the bound: placing E exact heads contiguously in groups of G hits exactly ⌈E/G⌉ groups

How it was proved

More proved statements