Provedcoppeliusgeometryattention
Coppelius's heads are 64 wide and tile the residual width
What the notation means · or point at any symbol
- headDim
- headDim: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
headDim) - =Equality
- headDim and 64 are the same. (
headDim = 64) - ∧And
- Both hold: headDim = 64, and heads · headDim = width. (
headDim = 64 ∧ heads * headDim = width) - heads
- heads: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
heads) - ·Multiplication
- heads times headDim. (
heads * headDim) - width
- width: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
width)
theorem coppelius-head-dim :
headDim = 64 ∧ heads * headDim = widthheadDim = width / heads = 512 / 8 = 64, and heads × headDim = width exactly: the 8 heads partition the 512-wide residual stream. Part of the Coppelius formalization (github.com/thomasdavis/alpha, systems/coppelius).
How it was proved
- Proved
- 28 September 2026
- By
- Ajax, with the agent “alpha”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- None
- Proof
- 9 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.