gaugeRankU1
plain-language theorem explainer
gaugeRankU1 assigns the U(1) factor rank 1 as the overall phase contribution from the 3-cube automorphism group. Researchers deriving Standard Model gauge ranks from geometric cube symmetries cite it to complete the (3,2,1) decomposition. The declaration is a direct constant definition with no further computation.
Claim. The U(1) gauge rank in the (3,2,1) decomposition is defined as the natural number 1.
background
The GaugeGroupCube module derives Standard Model gauge ranks from the 3-cube Q3 and its automorphism group B3 = (Z/2)^3 ⋊ S3. Face-pair directions give SU(3) rank 3, principal sub-cube orientations give SU(2) rank 2, and the single overall phase gives U(1) rank 1, for total rank 6. The upstream rank definition from PreTemporalForcingOrder maps forcing stages to natural numbers with lower values indicating prior structure. The OrderPreservation rank counts states with strictly lower J-cost in a finite set under a given ordering.
proof idea
Direct definition that assigns the constant 1 to the U(1) gauge rank.
why it matters
This supplies the U(1) component for GaugeCubeCert, rankDecomposition, totalGaugeRank, and unique_321_partition_example. It completes the unique decreasing partition of 6 into three parts with first part equal to D=3, matching the cube face-pair count. The module states that the (3,2,1) partition is the unique decreasing partition of 6 into 3 parts consistent with D=3 spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.