smHyperchargeCert
plain-language theorem explainer
Bundles the Standard Model hypercharge layer in sixth-units into one certificate: six Weyl multiplets, 16 states per generation, 48 across three generations, vanishing SU(3)^2U(1), SU(2)^2U(1), gravitational-U(1) and U(1)^3 anomalies, plus quark/lepton electric charges and Higgs Y6=3. Anyone citing the cube-to-SM gauge bridge will point here. The body is a pure structure instance wiring already-proved native_decide lemmas.
Claim. There is a certificate recording that the cube-completion hypercharge layer has exactly six Weyl multiplets; one generation totals $16$ Weyl states and three generations total $48=|B_3|$; the integer anomalies $\mathrm{SU}(3)^2U(1)$, $\mathrm{SU}(2)^2U(1)$, gravitational $U(1)$, and $U(1)^3$ all vanish in $Y_6=6Y$ units; the quark doublet has electric charges $Q_6=(4,-2)$ and the lepton doublet $Q_6=(0,-6)$; and the Higgs hypercharge is $Y_6=3$.
background
The module sits after GaugeLieCompletionFromCube, which already forces the compact gauge skeleton $SU(3)\times SU(2)\times U(1)$ with recognition-axis counts $(3,2,1)$ and carrier counts $(8,3,1)$. The remaining question is whether SM fermion multiplets and hypercharges fit the same cube-completion arithmetic.
Hypercharges are written in the canonical sixth-unit $Y_6=6Y$. One left-handed generation (including a sterile/right-handed neutrino at $Y_6=0$) is the six multiplets $Q_L$ (mult.\ 6, $Y_6=1$), $u^c_L$ (3, $-4$), $d^c_L$ (3, $2$), $L_L$ (2, $-3$), $e^c_L$ (1, $6$), $\nu^c_L$ (1, $0$). Their multiplicities sum to $16$ Weyl states; three generations give $48$, matching $|B_3|=|\mathrm{SignedPerm},3|$.
The structure SMHyperchargeCert packages the counting equalities, the four anomaly vanishings, the electric-charge identities for quark and lepton doublets (via $Q=T_3+Y$), and the Higgs value $Y_6=3$. The module is explicit that this is the anomaly-free SM layer in cube units, not a uniqueness proof for the charges.
proof idea
Pure structure construction: each field of SMHyperchargeCert is filled by a named sibling theorem. Multiplet count uses weylMultiplet_count; generation totals use generationWeylStateCount_eq_16 and threeGenerationWeylStateCount_eq_48; the four anomaly fields use su3SquaredU1Anomaly6_eq_zero, su2SquaredU1Anomaly6_eq_zero, gravitationalU1Anomaly6_eq_zero, and cubicU1Anomaly6_eq_zero (all native_decide on finite integer sums); doublet electric charges use quark_doublet_charges and lepton_doublet_charges; Higgs uses higgsHypercharge6_eq (rfl to $3$). No new reasoning occurs at this site.
why it matters
This certificate is the concrete SM hypercharge surface that the forcing chain hands to the gauge bridge. Downstream, t8_to_gauge_standard_model_bridge_holds routes T8 (D=3 forced) through the cube/spinor skeleton into gauge and Standard Model theorem surfaces; the hypercharge layer is part of that bridge payload.
In the Recognition framework it closes the P0-S2-01 punchlist item after the Lie-factor skeleton: once D=3 and the eight-tick/cube geometry are in place, the SM multiplet content and anomaly-free $Y_6$ arithmetic sit in the same units. It does not claim the hypercharges are uniquely forced by the functional equation; it only certifies that the textbook anomaly-free assignment is exactly representable and cancelled in cube-completion integers. That distinction matters for any later uniqueness or derivation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.