Encyclopedia Foundation Foundation Smhypercharge From Cube Three Generation Weyl State Count Eq 48
ARTICLE 3 claims 2 theorems 1 model
Foundation Smhypercharge From Cube Three Generation Weyl State Count Eq 48
A machine-checked theorem shows that three generations of Standard Model particles contain exactly 48 Weyl states, matching the size of a cube's signed permutation group.
The 48-state count
In particle physics, a Weyl state is a single left-handed or right-handed fermion component with a definite chirality, essentially one independent particle degree of freedom. The Standard Model's one generation of fermions, including the right-handed neutrino, contains 16 such states: 6 for the quark doublet, 3 each for the up and down conjugate singlets, 2 for the lepton doublet, and 1 each for the electron and neutrino conjugates. Three generations therefore contain 48 states in total.
The Recognition Science framework's machine-checked library of formal theorems proves this count exactly. The theorem threeGenerationWeylStateCount_eq_48 establishes that three times the one-generation count equals 48, and that this number equals the size of a signed permutation group on three elements, a finite group of order 48. The proof is a direct computation, verified without any axioms beyond the standard logical ones.
This count is not an isolated curiosity. The same library proves that the hypercharge assignments for these multiplets, expressed in units of one-sixth, exactly cancel all four relevant anomaly sums: the SU(3)²U(1), SU(2)²U(1), gravitational-U(1), and U(1)³ anomalies. These cancellations are required for the Standard Model to be mathematically consistent as a quantum field theory, and they hold in integer arithmetic without approximation.
What the theorem does not claim is that these hypercharges are uniquely forced by the framework. The library's own documentation states this plainly: the construction is the exact anomaly-free Standard Model hypercharge layer expressed in the cube completion's one-sixth unit, not a proof of uniqueness. The framework models the Standard Model structure; it does not yet derive that this structure is the only possible one.
The significance is that a purely combinatorial object, the signed permutation group on three elements, has the same size as the fermionic content of three generations. This match is established as a theorem, not conjectured. It gives a concrete sense in which the framework's cube-based structure aligns with the Standard Model's particle content, while leaving open the deeper question of whether that alignment is forced or coincidental.
THEOREM threeGenerationWeylStateCount_eq_48 · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
theorem threeGenerationWeylStateCount_eq_48 :
threeGenerationWeylStateCount = Fintype.card (GaugeFromCube.SignedPerm 3) := by
rw [GaugeFromCube.cube_aut_order]
native_decide
THEOREM su3SquaredU1Anomaly6_eq_zero · su2SquaredU1Anomaly6_eq_zero · gravitationalU1Anomaly6_eq_zero · cubicU1Anomaly6_eq_zero · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
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
MODEL smHyperchargeCert · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
def smHyperchargeCert : SMHyperchargeCert where
six_multiplets := weylMultiplet_count
one_generation_16 := generationWeylStateCount_eq_16
three_generations_b3 := threeGenerationWeylStateCount_eq_48
su3_anomaly_zero := su3SquaredU1Anomaly6_eq_zero
su2_anomaly_zero := su2SquaredU1Anomaly6_eq_zero
gravitational_anomaly_zero := gravitationalU1Anomaly6_eq_zero
cubic_anomaly_zero := cubicU1Anomaly6_eq_zero
quark_charges := quark_doublet_charges
lepton_charges := lepton_doublet_charges
higgs_y6 := higgsHypercharge6_eq
What this page does not claim
The theorem does not prove that the Standard Model hypercharges are the only possible ones consistent with the cube completion. The theorem does not derive the number of generations; it assumes three and counts their states. The theorem does not establish any physical prediction beyond the mathematical identity of the counts.
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:
- What would it take to prove that the Standard Model hypercharge assignments are uniquely forced by the cube completion?
- Does the signed permutation group on three elements carry additional structure beyond its size that corresponds to Standard Model symmetries?
- How does the 48-state count relate to the framework's derivation of three spatial dimensions?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM threeGenerationWeylStateCount_eq_48 · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
theorem threeGenerationWeylStateCount_eq_48 : threeGenerationWeylStateCount = Fintype.card (GaugeFromCube.SignedPerm 3) := by rw [GaugeFromCube.cube_aut_order] native_decideThe theorem threeGenerationWeylStateCount_eq_48 establishes that three times the one-generation count equals 48, and that this number equals the size of a signed permutation group on three elements. threeGenerationWeylStateCount_eq_48 · IndisputableMonolith/Foundation/SMHyperchargeFromCube.leanTHEOREM su3SquaredU1Anomaly6_eq_zero · su2SquaredU1Anomaly6_eq_zero · gravitationalU1Anomaly6_eq_zero · cubicU1Anomaly6_eq_zero · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
theorem su3SquaredU1Anomaly6_eq_zero : su3SquaredU1Anomaly6 = 0 := by native_decidetheorem su2SquaredU1Anomaly6_eq_zero : su2SquaredU1Anomaly6 = 0 := by native_decidetheorem gravitationalU1Anomaly6_eq_zero : gravitationalU1Anomaly6 = 0 := by native_decidetheorem cubicU1Anomaly6_eq_zero : cubicU1Anomaly6 = 0 := by native_decideThe same library proves that the hypercharge assignments exactly cancel all four relevant anomaly sums. su3SquaredU1Anomaly6_eq_zero · su2SquaredU1Anomaly6_eq_zero · gravitationalU1Anomaly6_eq_zero · cubicU1Anomaly6_eq_zero · IndisputableMonolith/Foundation/SMHyperchargeFromCube.leanMODEL smHyperchargeCert · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean
def smHyperchargeCert : SMHyperchargeCert where six_multiplets := weylMultiplet_count one_generation_16 := generationWeylStateCount_eq_16 three_generations_b3 := threeGenerationWeylStateCount_eq_48 su3_anomaly_zero := su3SquaredU1Anomaly6_eq_zero su2_anomaly_zero := su2SquaredU1Anomaly6_eq_zero gravitational_anomaly_zero := gravitationalU1Anomaly6_eq_zero cubic_anomaly_zero := cubicU1Anomaly6_eq_zero quark_charges := quark_doublet_charges lepton_charges := lepton_doublet_charges higgs_y6 := higgsHypercharge6_eqThe library's own documentation states plainly that the construction is not a proof that these hypercharges are uniquely forced. smHyperchargeCert · IndisputableMonolith/Foundation/SMHyperchargeFromCube.lean