GPPVerify: Lean 4 Formalization of the ONON Framework

12 Standard Model — Three Generations

12.1 Division Algebra Tower

Lemma 12.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.

Gap: full Hurwitz theorem not yet in Mathlib 4.19.0.

Theorem 12.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 12.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\).