gaugeCubeCert
plain-language theorem explainer
The definition constructs a certified instance of the gauge group cube certificate, confirming that the ranks of SU(3), SU(2), and U(1) arise as 3, 2, and 1 from the face pairs and orientations of the 3-cube and sum to 6. A researcher deriving the Standard Model gauge group from spatial symmetries would cite this to close the rank calculation in the Recognition Science framework. It assembles the required fields by direct substitution of the total rank theorem, the decomposition lemma, and the face-pair equality.
Claim. The gauge group cube certificate is the structure whose total rank field equals the sum of the SU(3), SU(2), and U(1) ranks being 6, whose decomposition field is the triple (3, 2, 1), whose SU(3) rank field equals the number of face-pair directions on the 3-cube, and whose decreasing partition field asserts the inequalities 3 ≥ 2 ≥ 1.
background
Recognition Science derives the (3, 2, 1) rank decomposition of the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube, B₃ = (ℤ/2)³ ⋊ S₃. The cube possesses three face-pair directions that fix the SU(3) rank at 3, two principal sub-cube orientations that fix the SU(2) rank at 2, and one overall phase that fix the U(1) rank at 1, for a total rank of 6. The (3, 2, 1) partition is the unique decreasing partition of 6 into three parts with the first part equal to the spatial dimension D = 3.
proof idea
The definition is a record constructor that populates the four fields of the GaugeCubeCert structure. It assigns the total rank field to the theorem totalGaugeRank, the decomposition field to the theorem rankDecomposition, the SU(3) rank equality to the theorem su3_rank_eq_face_pairs, and the decreasing partition to a pair of decidable propositions verified by the decide tactic.
why it matters
This definition supplies the concrete certificate that realizes the (3, 2, 1) rank structure of the Standard Model gauge group from the symmetries of the 3-cube in the Recognition Science framework. It completes the geometric derivation of the gauge ranks consistent with D = 3 spatial dimensions. The module extends the GaugeFromCube construction and incorporates the Wolfenstein A prediction, though no downstream theorems yet depend on this certificate. It anchors the T8 step of the forcing chain where the spatial dimension fixes the leading rank in the decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.