Foundation Smhypercharge From Cube

The hypercharge layer

Hypercharge is the quantum number that distinguishes particles of the same color and weak isospin but different electric charge. In the Standard Model of particle physics, each left-handed fermion carries a rational value of hypercharge Y, and the electric charge Q is the sum of hypercharge and the third component of weak isospin. The known fermions of one generation, including the right-handed neutrino, come in six multiplets with multiplicities 6, 3, 3, 2, 1, and 1, totaling 16 Weyl states. Their hypercharges, when multiplied by 6 to clear denominators, are the integers 1, -4, 2, -3, 6, and 0.

What the Recognition Science framework's machine-checked library of formal theorems establishes is that these assignments, expressed in the cube completion's 1/6 unit, form an exact anomaly-free layer. The four anomaly sums that must vanish for a consistent quantum field theory, the SU(3)²U(1), SU(2)²U(1), gravitational-U(1), and U(1)³ anomalies, all cancel in integer arithmetic. The library verifies these cancellations by direct computation, with no unproved axioms. It also verifies the generation count: one generation has 16 Weyl states, and three generations have 48, a number that matches the order of the signed permutation group on three elements, the cube's symmetry group.

This is a representation result, not a derivation. The module does not establish that these hypercharges are uniquely forced by the cube completion. It shows that the Standard Model's hypercharge layer, including the Higgs doublet with Y6 = 3, fits exactly into the cube's 1/6 unit with all anomaly sums vanishing. The electric charges that follow, such as the up quark's +2/3 and the electron's -1, emerge from the same sixth-unit arithmetic. The framework models this as a certificate: a structure that packages the six multiplets, the 16-state count, the 48-state three-generation count, the four anomaly cancellations, the quark and lepton charges, and the Higgs hypercharge as one verified object.

theorem su3SquaredU1Anomaly6_eq_zero : su3SquaredU1Anomaly6 = 0 := by
  native_decide

theorem su2SquaredU1Anomaly6_eq_zero : su2SquaredU1Anomaly6 = 0 := by
  native_decide

theorem gravitationalU1Anomaly6_eq_zero : gravitationalU1Anomaly6 = 0 := by
  native_decide

theorem cubicU1Anomaly6_eq_zero : cubicU1Anomaly6 = 0 := by
  native_decide

theorem generationWeylStateCount_eq_16 : generationWeylStateCount = 16 := by
  native_decide

theorem threeGenerationWeylStateCount_eq_48 :
    threeGenerationWeylStateCount = Fintype.card (GaugeFromCube.SignedPerm 3) := by
  rw [GaugeFromCube.cube_aut_order]
  native_decide

What this page does not claim

The hypercharge values are uniquely derived from the cube completion. The framework predicts any new particles beyond the Standard Model's 16 Weyl states per generation. The anomaly cancellations are derived from the cube's geometry rather than verified as an exact fit.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: