smHyperchargeDescription
plain-language theorem explainer
The definition supplies a textual assertion that hypercharges cancel within each generation to secure anomaly freedom. Researchers deriving gauge symmetries from ledger redundancy in Recognition Science would cite it when discussing Standard Model consistency conditions. It is realized as a direct string assignment with no computation or lemmas.
Claim. The Standard Model hypercharge assignments satisfy the per-generation cancellation condition $3(2Y_{u_L} + Y_{u_R} + Y_{d_R}) + (Y_{e_L} + Y_{e_R} + Y_{ν_L} + Y_{ν_R}) = 0$, with explicit values $Y_{u_L}=1/6$, $Y_{u_R}=2/3$, $Y_{d_R}=-1/3$, $Y_{e_L}=-1/2$, $Y_{e_R}=-1$, $Y_{ν_L}=-1/2$, $Y_{ν_R}=0$.
background
The QFT.GaugeInvariance module derives gauge invariance from ledger redundancy, where distinct representations encode identical physics and local phase freedom is compensated by gauge fields. Upstream results supply the cost function from MultiplicativeRecognizerL4 as the derived cost of its comparator on positive ratios, and the cost from ObserverForcing as the J-cost of any recognition event. The module context frames Yang-Mills dynamics as arising from information cost rather than being postulated.
proof idea
The declaration is a direct string assignment of the literal describing hypercharge cancellation for anomaly freedom.
why it matters
The definition supplies the anomaly-freedom condition required for the gauge-symmetry emergence argument in the module, which targets a Nature Physics paper on gauge symmetry from information redundancy. It anchors the Standard Model's consistency within the Recognition Science ledger framework without invoking the forcing chain or RCL directly. No downstream theorems reference it, so it functions as explanatory scaffolding for the gauge-invariance derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.