GaugeCubeCert
plain-language theorem explainer
GaugeCubeCert packages the rank relations for the Standard Model gauge group as derived from the 3-cube geometry. A physicist tracing gauge symmetries to discrete spatial structures would cite this certificate. The structure definition collects the sum-to-six property, the explicit (3,2,1) split, the equality of the SU(3) rank to the cube face-pair count, and the decreasing order of the ranks.
Claim. A structure asserting that the sum of the SU(3), SU(2), and U(1) gauge ranks equals 6, that these ranks are respectively 3, 2, and 1, that the SU(3) rank equals the number of face-pair directions on the 3-cube, and that the ranks form a decreasing sequence.
background
In the Gauge Group from 3-Cube module, Recognition Science obtains the Standard Model gauge ranks from the automorphism group of the 3-cube. The cube Q₃ = {0,1}³ yields three face-pair directions, two principal sub-cube orientations, and one overall phase, giving the (3,2,1) decomposition with total rank 6. The upstream definitions fix the SU(3) rank at 3, the SU(2) rank at 2, the U(1) rank at 1, and the cube face-pair count at 3, where the latter counts the face-pair directions in D = 3 spatial dimensions.
proof idea
This declaration is a structure definition with no proof body. It directly encodes the four required properties using the constant definitions for the SU(3), SU(2), and U(1) ranks together with the cube face-pair count. The downstream construction instantiates the structure with the total rank sum, the explicit decomposition, the equality to face pairs, and a decidable decreasing check.
why it matters
GaugeCubeCert supplies the certified rank decomposition that feeds the gaugeCubeCert instance. It realizes the module claim that the (3,2,1) partition is the unique decreasing partition of 6 consistent with D=3 cube face-pairs. In the Recognition Science framework this closes the step from T8 (D=3) to the gauge group ranks via the cube automorphism group B₃ = (ℤ/2)³ ⋊ S₃.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.