SMHyperchargeCert
plain-language theorem explainer
Certificate that packages the Standard Model hypercharge layer in sixth-units on the cube completion: six left-handed Weyl multiplets, 16 states per generation, three-generation count equal to |B_3|, vanishing SU(3)^2 U(1), SU(2)^2 U(1), gravitational-U(1) and U(1)^3 anomalies, quark and lepton electric charges in sixth-units, and Higgs Y_6 = 3. Bridge theorems from T8 into the gauge SM skeleton cite it. As a structure it has no proof body; an inhabitant fills each field by a named equality lemma.
Claim. A certificate asserting: exactly six left-handed Weyl multiplets; one generation has $16$ Weyl states; three generations match $|B_3|=|\mathrm{SignedPerm}\,3|$; the scaled anomalies $\mathrm{SU}(3)^2U(1)$, $\mathrm{SU}(2)^2U(1)$, gravitational-$U(1)$, and $U(1)^3$ all vanish; electric charges in sixth-units satisfy $Q_6(u)=4$, $Q_6(d)=-2$ on the quark doublet and $Q_6(\nu)=0$, $Q_6(e)=-6$ on the lepton doublet; and the Higgs has $Y_6=3$ (i.e. $Y=1/2$).
background
After the cube-completion gauge skeleton $\mathrm{SU}(3)\times\mathrm{SU}(2)\times U(1)$ with recognition-axis counts $(3,2,1)$ and carrier counts $(8,3,1)$, this module asks whether SM fermion multiplets and hypercharges live in the same units. Hypercharges are written as integers $Y_6=6Y$.
One left-handed generation (including a sterile/right-handed neutrino as the $Y=0$ completion) is the six-type multiplet list: quark doublet (mult.\ 6, $Y_6=1$), $u^c$ (3, $-4$), $d^c$ (3, $2$), lepton doublet (2, $-3$), $e^c$ (1, $6$), $\nu^c$ (1, $0$). Multiplicities sum to $16$ Weyl states. Anomaly sums $\mathrm{SU}(3)^2U(1)$, $\mathrm{SU}(2)^2U(1)$, gravitational-$U(1)$, and $U(1)^3$ are defined as integer linear combinations of the $Y_6$ values (cubic anomaly scaled by $6^3$).
Electric charge in sixth-units is $Q_6=T_{3,6}+Y_6$. The hyperoctahedral group $B_3$ (signed permutations on three coordinates) supplies the three-generation cardinality check. Module status: zero sorry, zero axiom.
proof idea
Structure definition, not a proved theorem: each field is a bare proposition. No tactics or term proof appear on the declaration itself.
The canonical inhabitant later fills the fields by sibling lemmas: multiplet cardinality, the equality of the generation state count to $16$, the three-generation count to $|B_3|$, the four anomaly-vanishing equalities, the two electric-charge conjunctions, and the constant Higgs $Y_6=3$. Those lemmas are ordinary rfl/arithmetic reductions on the explicit integer tables.
why it matters
Closes the hypercharge layer of punchlist item P0-S2-01: the anomaly-free SM fermion content expressed in the cube completion's $1/6$ unit, after the gauge-factor skeleton. The module doc is explicit that this is representation, not uniqueness: hypercharges are not yet forced.
Downstream, the inhabited certificate is the witness consumed by the T8-to-gauge-Standard-Model bridge in the unified forcing chain (T8 forces $D=3$, which supplies the cube whose completion carries this layer). Parent use sites are the concrete certificate value and that bridge structure.
Framework landmarks: sits after T8 ($D=3$) and the cube automorphism group $B_3$; feeds the gauge SM routing without touching $\phi$-ladder masses, $\alpha$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.