cube_matches_sm
plain-language theorem explainer
The cube-derived gauge ranks equal the Standard Model ranks (3,2,1). Researchers deriving the Standard Model gauge group from 3-cube symmetry cite this to close the rank-matching step in the P-014 derivation. The proof is a one-line wrapper that applies extensionality on Fin 3 followed by exhaustive case analysis on the three indices.
Claim. Let $r_C : {Fin} 3 → ℕ$ be the tuple of fundamental representation dimensions extracted from the color, weak, and hypercharge layers of the 3-cube. Let $r_{SM} = (3,2,1)$. Then $r_C = r_{SM}$.
background
Module P-014 derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B₃ of the 3-cube Q₃. The cube_gauge_ranks definition assembles the three fundamental representation dimensions from the color layer (S₃ action on face-pairs), weak layer (even sign flips), and hypercharge layer. The sm_gauge_ranks definition is the constant tuple (3,2,1). Upstream results include SpectralEmergence.of, which states that Q₃ simultaneously forces gauge content with sector dimensions summing to 6, and PhiForcingDerived.of together with LedgerFactorization.of that calibrate the underlying J-cost and forcing chain.
proof idea
The proof is a one-line wrapper. It applies the extensionality tactic on the Fin 3 index, then uses fin_cases to reduce to three trivial equalities that are discharged by rfl.
why it matters
This equality is the second conjunct inside the gauge_group_certificate theorem, which certifies that B₃ = (ℤ/2ℤ)³ ⋊ S₃ forces the Standard Model ranks. It sits downstream of the forcing chain T5–T8 (J-uniqueness, phi fixed point, eight-tick octave, D=3) and is used by mass_gap_from_forcing_chain and yang_mills_gap_cert to close the gauge sector of the Yang-Mills mass gap certificate. The result supplies the missing SU(2) and U(1) ranks once the SU(3) color factor is already obtained from face-pair counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.