Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SMHyperchargeFromCube

show as:
view Lean formalization →

Defines Standard Model hypercharge assignments and left-handed Weyl multiplet content from the completed 3-cube gauge data. Counts one generation as 16 Weyl states and three generations as 48, and checks the SU(3)^2 U(1)_Y anomaly vanishes in sixfold units. Cited by anyone assembling the SM fermion sector inside the forcing chain. Structure is mostly definitions plus short equality and anomaly lemmas.

claimFrom the completed 3-cube gauge layer, assign SM hypercharges (in units of $1/6$) to one left-handed generation of Weyl multiplets, including the Higgs value; prove the generation has $16$ Weyl states ($48$ for three generations) and that the $SU(3)^2 U(1)_Y$ anomaly coefficient vanishes.

background

Recognition Science forces spatial dimension $D=3$ and an eight-tick octave from the cost foundation (T7, T8). The upstream module GaugeLieCompletionFromCube starts punchlist item P0-S2-01: the cube already forces $B_3$ layer counts (axis permutations $3$, even sign-flip completion $2$), supplying the discrete skeleton for gauge Lie data.

This module turns that skeleton into SM fermion bookkeeping. A Weyl multiplet is a left-handed chiral multiplet of the residual gauge algebra; hypercharge is recorded in sixths so that all SM values are integers. Generation state count packages quarks, leptons, and conjugates into a single integer invariant of the cube labeling.

Local setting is Foundation: pure combinatorial and representation facts, no continuum QFT dynamics yet. Anomaly coefficients are the usual cubic and mixed traces evaluated on the assigned charges.

proof idea

Definition-heavy module. Enumerated multiplet and hypercharge tables are introduced as data; equalities such as generation count $=16$, three-generation count $=48$, and Higgs hypercharge in sixths are one-line rewrites or rfl-style checks against those tables. The mixed anomaly $SU(3)^2 U(1)_Y$ is a finite integer sum over the multiplet list and is shown to cancel by direct evaluation. No deep tactic search; the work is faithful transcription of cube-derived charges into SM notation plus arithmetic closure.

why it matters in Recognition Science

Feeds UnifiedForcingChain, which claims all of T0-T8 are forced from the Recognition Composition Law and cost foundation. Without a cube-native hypercharge and anomaly-safe generation count, the chain cannot land the Standard Model fermion sector on the same discrete geometry that forces $D=3$ and the eight-tick period. Closes the bookkeeping half of gauge completion after GaugeLieCompletionFromCube supplies the $B_3$ counts. Touches the broader program of deriving $\alpha$ and mass-ladder inputs from the same $\phi$-structured cube, though this file itself stops at multiplet arithmetic and anomaly vanishing.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (25)