Pith. sign in
module module moderate

IndisputableMonolith.Foundation.GaugeGroupCube

show as:
view Lean formalization →

The module defines the ranks of the three standard model gauge groups SU(3), SU(2), U(1) along with their sum and a cube-face decomposition. A particle physicist working in Recognition Science would cite these when embedding the gauge sector. The module consists entirely of definitions and elementary equalities with no tactic proofs.

claimThe module introduces the gauge ranks $\mathrm{rank}(SU(3))$, $\mathrm{rank}(SU(2))$, $\mathrm{rank}(U(1))$, the total rank, the 3-2-1 partition, and the cube face-pair relation certified by GaugeCubeCert.

background

Recognition Science places gauge structure inside the Foundation layer that precedes the forcing chain T0-T8. The module supplies the concrete ranks for the standard-model gauge group SU(3)×SU(2)×U(1) and encodes them as a geometric cube whose six faces correspond to the rank sum. Sibling definitions include gaugeRankSU3, gaugeRankSU2, gaugeRankU1, totalGaugeRank, rankDecomposition, cubeFacePairs, and the certificate GaugeCubeCert.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

These rank definitions supply the gauge-sector input required by later Recognition Science results on the standard-model spectrum and the D=3 spatial structure. The module therefore sits directly beneath any theorem that invokes the 3-2-1 gauge partition inside the unified forcing chain.

scope and limits

declarations in this module (11)