unique_321_partition_example
plain-language theorem explainer
The declaration confirms the gauge ranks decompose as 3 for SU(3), 2 for SU(2), and 1 for U(1) while satisfying the strict decreasing order. Model builders deriving the Standard Model gauge group from 3-cube geometry would cite this partition when checking consistency with spatial dimension D=3. The proof reduces to a direct decidable check on the three constant definitions.
Claim. $r_3 = 3$, $r_2 = 2$, $r_1 = 1$ with $r_3 > r_2 > r_1$, where the ranks are the face-pair, sub-cube, and phase contributions from the 3-cube.
background
The module constructs the Standard Model gauge group from the automorphism group of the 3-cube Q₃. Three face-pair directions yield rank 3 for SU(3), two principal sub-cube orientations yield rank 2 for SU(2), and one overall phase yields rank 1 for U(1). The sibling definitions fix these values directly: gaugeRankSU3 := 3, gaugeRankSU2 := 2, gaugeRankU1 := 1, with total rank 6 matching the rank of SU(3)×SU(2)×U(1).
proof idea
The proof is a one-line wrapper that applies the decidable equality tactic to the conjunction of the three equalities and two inequalities on the constant natural numbers.
why it matters
The result verifies the unique decreasing partition of total rank 6 into three parts whose largest entry equals D=3, the spatial dimension fixed by the Recognition Science forcing chain at T8. It anchors the gauge-group derivation inside the cube automorphism construction and supplies the concrete (3,2,1) numbers used by downstream rank-decomposition statements. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.