unique_321_partition_example
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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the partition outside this explicit example.
- Does not derive the rank numbers from the cube automorphism group.
- Does not link the ranks to the phi-ladder or mass formula.
formal statement (Lean)
40theorem unique_321_partition_example :
41 gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1 ∧
42 gaugeRankSU3 ≥ gaugeRankSU2 ∧ gaugeRankSU2 ≥ gaugeRankU1 := by
proof body
Decided by rfl or decide.
43 decide
44
45/-- Cube face-pair count = 3 (D=3 spatial dimension). -/