threeGenerationWeylStateCount
plain-language theorem explainer
Three Standard Model generations contribute 48 Weyl fermion states under the cube-completion multiplet count (three times the 16 states of one generation). Anyone matching fermion content to the order of the signed-permutation group B3 cites this constant. It is a one-line product definition, not a derived theorem.
Claim. The total number of Weyl fermion states across three generations is defined to be $3$ times the one-generation Weyl state count (itself $6+3+3+2+1+1=16$ from the left-handed SM multiplets including a sterile neutrino).
background
The module places the Standard Model hypercharge layer on the same cube-completion units that already force the gauge skeleton $SU(3)\times SU(2)\times U(1)$. Hypercharges are written as integers $Y_6=6Y$ so anomaly sums stay in exact integer arithmetic.
One left-handed generation is packaged as six Weyl multiplets: quark doublet (mult. 6, $Y_6=1$), up and down conjugates (3 each), lepton doublet (2), electron conjugate (1), and sterile neutrino (1, $Y_6=0$). Their multiplicities sum to the upstream constant generationWeylStateCount, documented as $16$ Weyl states per generation.
The present definition simply scales that one-generation tally by three. The module explicitly notes this is an anomaly-free SM layer in $1/6$ units, not yet a uniqueness proof for the hypercharge assignments.
proof idea
Pure definition: the natural number is the product of the literal coefficient $3$ with the already-defined one-generation Weyl state count. No tactics, no lemmas, no computation beyond that multiplication.
why it matters
This constant is the three-generation side of the equality proved next: it equals the cardinality of the signed-permutation group on three letters (order of $B_3$), which is $48$. That equality is a field of SMHyperchargeCert, the module's certificate packing multiplet count, one- and three-generation tallies, and vanishing $SU(3)^2U(1)$ anomaly.
Downstream it is also referenced by T8_To_GaugeStandardModel_Bridge in the unified forcing chain, the structure that routes the T8 dimension force ($D=3$) into the gauge and Standard Model layer. In the Recognition framework it therefore sits on the path from cube dimension to SM fermion accounting, while the module itself flags that hypercharge uniqueness remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.