proofs
Provedalphabaguettegeometry

Baguette geometry: GQA 9:3 heads of width 64 tile the 576 residual, and the model has 320,956,992 parameters

576=9⋅64∧9 mod 3=0∧65536⋅576+80(576(2(9⋅64)+2(3⋅64))+(3(576⋅1536)+2⋅576))+576=320956992∧∀k:Fin⁡ 3, ∣filter⁡(univ⁡)(h↦val⁡(h)3=val⁡(k))∣=3\begin{aligned} & 576 \mathrel{\htmlData{mx=2}{=}} \htmlData{mx=1}{9 \cdot 64} \\ & \htmlData{mx=0}{\land} \htmlData{mx=3}{9 \bmod 3} \mathrel{\htmlData{mx=4}{=}} 0 \\ & \htmlData{mx=0}{\land} \htmlData{mx=20}{\htmlData{mx=19}{\htmlData{mx=6}{65536 \cdot 576} + \htmlData{mx=18}{80(\htmlData{mx=17}{\htmlData{mx=12}{576(\htmlData{mx=11}{\htmlData{mx=8}{2(\htmlData{mx=7}{9 \cdot 64})} + \htmlData{mx=10}{2(\htmlData{mx=9}{3 \cdot 64})}})} + (\htmlData{mx=16}{\htmlData{mx=14}{3(\htmlData{mx=13}{576 \cdot 1536})} + \htmlData{mx=15}{2 \cdot 576}})})}} + 576} \\ & \quad \htmlData{mx=5}{=} 320956992 \\ & \htmlData{mx=0}{\land} \htmlData{mx=55}{\forall k : \htmlData{mx=54}{\htmlData{mx=53}{\operatorname{Fin}}\,3},\ \htmlData{mx=51}{\lvert \htmlData{mx=50}{\htmlData{mx=40}{\operatorname{filter}\left(\htmlData{mx=39}{\htmlData{mx=38}{\operatorname{univ}}}\right)}\left(\htmlData{mx=49}{h \mapsto \htmlData{mx=44}{\frac{\htmlData{mx=43}{\operatorname{val}\left(\htmlData{mx=42}{h}\right)}}{3}} \mathrel{\htmlData{mx=48}{=}} \htmlData{mx=47}{\operatorname{val}\left(\htmlData{mx=46}{k}\right)}}\right)} \rvert} \mathrel{\htmlData{mx=52}{=}} 3} \end{aligned}
What the notation means · or point at any symbol
=Equality
576 and 9 · 64 are the same. (576 = 9 * 64)
·Multiplication
9 times 64. (9 * 64)
modRemainder
The remainder when 9 is divided by 3. (9 % 3)
∧And
Both hold: 65536 · 576 + 80 · (576 · (2 · (9 · 64) + 2 · (3 · 64)) + …, and ∀ k, card(filter(univ)(h ↦ h.val/3 = k.val)) = 3. (65536 * 576 + 80 * (576 * (2 * (9 * 64)…)
+Addition
2 · (9 · 64) plus 2 · (3 · 64). (2 * (9 * 64) + 2 * (3 * 64))
∀For all
The statement after the comma holds for every k. (∀ k : Fin 3, ((Finset.univ : Finset (Fi…)
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)
|s|Cardinality
The number of elements of filter(univ)(h ↦ h.val/3 = k.val). (((Finset.univ : Finset (Fin 9)).filter …)
(x : T)Type ascription
univ read as a Finset(Fin(9)). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Finset.univ : Finset (Fin 9)))
e.ffilter
filter of univ: Lean's dot notation e.filter means filter applied to e. ((Finset.univ : Finset (Fin 9)).filter)
f(x)Function application
filter(univ) applied to h ↦ h.val/3 = k.val. Lean writes f x; papers write f(x). ((Finset.univ : Finset (Fin 9)).filter (…)
univ
Finset.univ: 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)
x ↦ f(x)Function (λ-abstraction)
The function sending h to h.val/3 = k.val. Lean writes fun x => …; papers write x ↦ …. (fun h => h.val / 3 = k.val)
e.fval
val of h: Lean's dot notation e.val means val applied to e. (h.val)
a/bDivision
h.val divided by 3. In Lean, dividing by 0 gives 0. (h.val / 3)

Baguette's grouped decoder geometry (Baguette.Model.baguetteGeometry = PleIAs/Baguettotron config: vocabulary 65536, context 4096, 80 layers, width 576, 9 query heads, 3 key/value heads, head width 64, feed width 1536, RoPE base 10000; Alpha commit e3330947, systems/baguette/src/Baguette/Model.alpha).

This checks the groupedDecoderAdmitted conditions that bind here: width = query heads × head width, and query heads divisible by KV heads. It checks the exact groupedDecoderParameterCount formula (tied embedding, Q/K/V/O, three gated-FF projections, two block gains per layer, final gain), which evaluates to the 320,956,992 quoted in GOAL-PRD.md. It also checks that the GQA map h ↦ h/3 assigns exactly three query heads to each KV head.

How it was proved

Proved
3 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.

More proved statements