Foundation Gauge Group Cube Rank Decomposition

The cube's gauge ranks

The Standard Model of particle physics groups its forces under a combined symmetry, written SU(3)×SU(2)×U(1). Each factor carries a rank, a whole number that counts the independent directions in its symmetry: 3 for the strong force, 2 for the weak force, and 1 for the electromagnetic phase. Their sum is 6.

In Recognition Science, the framework's machine-checked library of formal theorems derives this exact (3, 2, 1) split from the geometry of a three-dimensional cube. The cube has three pairs of opposite faces, giving the 3; two principal ways to slice it into sub-cubes, giving the 2; and one overall phase, giving the 1. The declaration rankDecomposition, a proved theorem in the library, establishes precisely these three equalities: the SU(3) rank is 3, the SU(2) rank is 2, and the U(1) rank is 1.

The result also states that (3, 2, 1) is the unique decreasing partition of 6 into three parts where the first part equals the spatial dimension 3. The library certifies this in a single structure, GaugeCubeCert, which bundles the total rank, the decomposition, the cube-face match, and the decreasing order into one machine-checked package.

What this does not claim is just as important. The theorem proves a numerical coincidence between cube geometry and gauge group ranks; it does not derive the full dynamics of the Standard Model, nor does it explain why these specific groups, rather than other rank-6 groups, govern nature. The physical bridge from cube symmetry to actual particle interactions remains an open target, not a proved consequence.

/-- Ranks match spatial dimension, sub-cube, and phase. -/
theorem rankDecomposition :
    gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1 := by
  exact ⟨rfl, rfl, rfl⟩

/-- The (3,2,1) partition is the unique decreasing partition of 6 into 3 parts
    where first part = D = 3. -/
theorem unique_321_partition_example :
    gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1 ∧
    gaugeRankSU3 ≥ gaugeRankSU2 ∧ gaugeRankSU2 ≥ gaugeRankU1 := by
  decide

def gaugeCubeCert : GaugeCubeCert where
  total_rank := totalGaugeRank
  decomp := rankDecomposition
  su3_from_cube := su3_rank_eq_face_pairs
  decreasing_partition := ⟨by decide, by decide⟩

What this page does not claim

The theorem does not derive the full Lagrangian or dynamics of the Standard Model. It does not prove that SU(3)×SU(2)×U(1) is the unique or necessary gauge group for nature. The physical bridge from cube symmetry to particle interactions remains open, not established.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/GaugeGroupCube.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: