generations_eq_dimension

formal source

 207abbrev Generation := Fin 3
 208
 209/-- **THEOREM**: The generation count matches the cube dimension. -/
 210theorem generations_eq_dimension : face_pairs 3 = 3 := three_generations
 211
 212/-! ## Part 4: Fermion Census — The 24 and 48 Theorems
 213
 214The total number of chiral fermion flavors is D × 2^D = 24.
 215The total fermionic state count is |Aut(Q₃)| = 48. -/
 216
 217/-- The chiral fermion flavor count: each sector contributes a number
 218    of flavors determined by matter_dim × generations × chiralities_per_sector. -/
 219def fermion_flavors : ℕ :=
 220  let quarks := SpectralSector.dim .color * face_pairs 3 * 2  -- 3 colors × 3 gen × 2 (u/d)
 221  let leptons := SpectralSector.dim .hypercharge * face_pairs 3 * 2  -- 1 × 3 gen × 2 (ν/e)
 222  quarks + leptons
 223
 224/-- **THEOREM**: 24 chiral fermion flavors.
 225    Quarks: 3 colors × 3 generations × 2 flavors (up/down) = 18
 226    Leptons: 1 × 3 generations × 2 flavors (ν/e) = 6
 227    Total: 24 -/
 228theorem fermion_count_24 : fermion_flavors = 24 := by
 229  native_decide
 230
 231/-- **THEOREM (D × 2^D identity)**: The fermion flavor count equals
 232    the cube dimension times its vertex count. -/
 233theorem fermions_eq_D_times_V : fermion_flavors = 3 * V 3 := by
 234  native_decide
 235
 236/-- **THEOREM (Aut(Q₃) / 2 identity)**: The fermion flavor count is
 237    half the automorphism group order (particle vs antiparticle). -/
 238theorem fermions_eq_half_aut : 2 * fermion_flavors = aut_order 3 := by
 239  native_decide
 240