fermion_flavors
plain-language theorem explainer
The definition computes the chiral fermion flavor count by adding the quark contribution (color sector dimension times three face pairs times two chiralities) to the lepton contribution (hypercharge sector dimension times three face pairs times two chiralities). Researchers deriving the Standard Model spectrum from the geometry of the three-dimensional cube would reference this count when linking Q3 symmetries to particle generations. The computation is a direct arithmetic expression using predefined sector dimensions and the face pair count.
Claim. The number of chiral fermion flavors is defined as $3 times 3 times 2 + 1 times 3 times 2$, where the factors 3 and 1 are the dimensions of the color and hypercharge sectors of the cube $Q_3$, the factor 3 is the number of face pairs, and the factor 2 accounts for chiralities per sector.
background
In the Spectral Emergence module the binary cube $Q_3$ with 8 vertices arises from the forced spatial dimension D=3. The SpectralSector inductive type partitions the symmetries into color (dimension 3, corresponding to SU(3)), weak (dimension 2), hypercharge (dimension 1), and conjugate (dimension 2). The face_pairs function, defined as D in the ParticleGenerations module, yields 3 for D=3, counting the pairs of opposite faces that determine the number of generations.
proof idea
The definition directly evaluates the sum of two products: the color sector dimension multiplied by face_pairs 3 and by 2, plus the hypercharge sector dimension multiplied by face_pairs 3 and by 2. No lemmas are invoked beyond the definitions of SpectralSector.dim and face_pairs; the body is a let-binding followed by addition.
why it matters
This definition supplies the numerical value 24 that is proved equal to the expected count in the downstream theorem fermion_count_24 and is used to establish the identities fermions_eq_D_times_V and fermions_eq_half_aut. It fills the step in the SpectralEmergenceCert that lists 24 fermion flavors as D times 2^D, confirming the link from T8 (D=3) through the Q3 geometry to the Standard Model particle content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.