sm_gauge_ranks
plain-language theorem explainer
The definition supplies the target gauge ranks (3, 2, 1) for the Standard Model in the cube symmetry derivation. Researchers matching the hyperoctahedral group B3 to SU(3) x SU(2) x U(1) cite this tuple when verifying equality with cube-derived ranks. It is introduced by direct assignment of the constant vector on Fin 3.
Claim. The Standard Model gauge rank tuple is the function $r : {0,1,2} → ℕ$ defined by $r(0)=3$, $r(1)=2$, $r(2)=1$.
background
The module derives the full Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3. B3 decomposes as (ℤ/2ℤ)³ ⋊ S3 of order 48, with S3 supplying the rank-3 color factor and the even-sign-flip subgroup (ℤ/2ℤ)² supplying the rank-2 weak factor. The local setting is P-014, which completes the gauge structure after earlier modules had accounted only for the SU(3) factor via face-pairs.
proof idea
This is a direct definition that assigns the array literal ![3, 2, 1] to the function on Fin 3. No lemmas or tactics are invoked.
why it matters
The definition anchors the P-014 certificate that cube symmetry reproduces the Standard Model gauge ranks. It is invoked by cube_matches_sm to equate the tuple with the cube-derived ranks, by total_gauge_dim to obtain the face-count identity 6, and by gauge_group_certificate. It feeds the Yang-Mills mass-gap chain that runs from the forcing order through T8 (D=3) and the Recognition Composition Law to the lattice gap Δ = J(φ).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.