threeGenerationWeylStateCount_eq_48
plain-language theorem explainer
Three SM generations (with sterile neutrinos) total 48 Weyl states, equal to the order of the 3-cube automorphism group B₃. The SM hypercharge certificate and the T8-to-gauge bridge cite this match. Proof rewrites the group order via cube_aut_order, then decides the numeric equality.
Claim. The three-generation Weyl state count equals the order of the signed-permutation group on three coordinates: $3\,N_{\mathrm{gen}}=|B_3|$, where $N_{\mathrm{gen}}=16$ is the one-generation Weyl count and $B_3=\mathrm{Aut}(Q_3)$ is the hyperoctahedral group of order $48$.
background
This module sits on the cube-completion gauge skeleton from GaugeLieCompletionFromCube: compact factors $SU(3)\times SU(2)\times U(1)$ with recognition-axis counts $(3,2,1)$. Hypercharges are written in sixth-units $Y_6=6Y$. One left-handed generation, including a sterile $\nu^c_L$ at $Y_6=0$, is packaged as six multiplets whose multiplicities sum to $16$ Weyl states ($Q_L$×6, $u^c$×3, $d^c$×3, $L_L$×2, $e^c$×1, $\nu^c$×1).
The three-generation count is defined as three times that one-generation total. Independently, SignedPerm 3 is the hyperoctahedral group $B_3$: permutations of three axes together with independent sign flips. Its order is the automorphism order of the 3-cube. Upstream, cube_aut_order records $|\mathrm{Aut}(Q_3)|=|B_3|=48$.
proof idea
Term-mode, two steps. Rewrite the right-hand side with cube_aut_order, which replaces Fintype.card (SignedPerm 3) by the numeral $48$. The left-hand side unfolds to $3\cdot\texttt{generationWeylStateCount}$; with the one-generation total fixed at $16$, native_decide closes $3\cdot 16=48$. No induction or case split.
why it matters
Closes the arithmetic link between three SM generations and the $D=3$ cube symmetry group forced at T8. Downstream, smHyperchargeCert packages it as the field three_generations_b3 alongside the one-generation count of $16$ and the integer anomaly vanishings in $Y_6$ units. Further up, t8_to_gauge_standard_model_bridge_holds routes gauge and SM surfaces through the canonical $D=3$ cube/spinor skeleton; this equality is the fermion-counting half of that bridge.
It does not claim the hypercharge assignment is uniquely forced (the module doc is explicit). It only shows the anomaly-free SM layer, counted in cube units, saturates $|B_3|$. That saturation is the bookkeeping step the forcing chain needs before uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.