GPPVerify: Lean 4 Formalization of the Shadow Framework

13 Standard Model — Three Generations

13.1 Division Algebra Tower

Lemma 13.1 Hurwitz Classification
#

The only normed division algebras over \(\mathbb {R}\) are \(\mathbb {R}\), \(\mathbb {C}\), \(\mathbb {H}\), \(\mathbb {O}\) (Hurwitz 1898). There are exactly \(3\) Cayley–Dickson doublings.

Status: carried as the hypothesis HurwitzDimensionHypothesis, not an axiom — the former axiom was retired on 2026-08-30 because no theorem consumed it. The dimension-counting content this chapter actually uses (cdStages_card, exactly_three_doublings, nda_dimensions_image, sedenion_dim_outside_nda_set) is proved outright, with no axiom.

Gap: the real classification is not in Mathlib 4.19.0 (only the complex Gelfand–Mazur theorem is). Note also that Mathlib’s NormedDivisionRing extends DivisionRing and is therefore associative, so \(\mathbb {O}\) does not inhabit it: as literally stated the \(8\) case is vacuous and the reachable content is the Frobenius classification \(\{ 1,2,4\} \). Any attempt to discharge this hypothesis should first restate it over a genuine composition-algebra structure.

Theorem 13.2 Three Generations from Division Algebras
#

The three Cayley–Dickson doublings \(\mathbb {R}\to \mathbb {C}\), \(\mathbb {C}\to \mathbb {H}\), \(\mathbb {H}\to \mathbb {O}\) correspond to exactly \(3\) fermion generations.

Theorem 13.3 Anomaly Cancellation Forces 3 Generations

With \(c_{4D}^{\mathrm{Weyl}} = 0\) and SM gauge group, anomaly cancellation (Boyle–Turok 2021) forces \(48 = 16 \times 3\) Weyl fermions, i.e., \(n_{\mathrm{gen}} = 3\).