pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.GaugeGroupCube

show as:
view Lean formalization →

GaugeGroupCube supplies the ranks for the three Standard Model gauge groups inside the Recognition Science foundation layer. It fixes gaugeRankSU3 at 3, gaugeRankSU2 at 2, gaugeRankU1 at 1, records their sum as totalGaugeRank, and supplies a rankDecomposition together with the relation that equates the SU(3) rank to the number of cube face pairs. The module consists solely of definitions and one illustrative example; no theorems or proofs appear.

claim$rank(SU(3))=3$, $rank(SU(2))=2$, $rank(U(1))=1$, total rank $6$, with decomposition into these three summands. The SU(3) rank equals the number of cube face pairs.

background

The module belongs to the Foundation domain and imports only Mathlib. It introduces the Lie-algebra ranks of the Standard Model gauge groups that arise after the forcing chain reaches T8 (D=3 spatial dimensions) and the eight-tick octave. Definitions include gaugeRankSU3, gaugeRankSU2, gaugeRankU1, totalGaugeRank, rankDecomposition, cubeFacePairs, and the equality su3_rank_eq_face_pairs that links the strong-group rank to cube geometry.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The ranks supplied here feed the gauge-group constructions that appear in later Recognition Science modules. They instantiate the 3-2-1 partition that matches the observed Standard Model and close the geometric link between SU(3) and the three-dimensional cube implied by T8. The unique_321_partition_example illustrates the partition that subsequent work on interactions and particle content relies upon.

scope and limits

declarations in this module (11)