color_layer
plain-language theorem explainer
The color_layer definition supplies the SU(3) color sector by recording fundamental representation dimension 3 and discrete order 6 drawn from the S3 axis-permutation factor of the cube automorphism group B3. Researchers assembling the Standard Model gauge ranks from Q3 symmetry cite this when forming the tuple (3,2,1) or verifying the dimension sum. It is a direct record construction that populates the GaugeLayer fields with the color parameters.
Claim. The color gauge layer is the record with name ``SU(3) color'', fundamental representation dimension $3$, and discrete order $6$.
background
The GaugeFromCube module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3, written as (Z/2Z)^3 ⋊ S3 of order 48. The GaugeLayer structure records for each sector its name, the dimension of its fundamental representation, and its discrete order; the doc-comment states that S3 acts on three axes to give fundamental dimension 3 and thereby the SU(3) color structure. This definition isolates the first of the three layers extracted from B3, following the earlier extraction of three generations and three colors from the same face-pair geometry.
proof idea
This is a direct definition that constructs the GaugeLayer record by literal assignment of the name ``SU(3) color'', fund_rep_dim to 3, and discrete_order to 6. No lemmas or tactics are invoked.
why it matters
The definition supplies the color component used by cube_gauge_ranks, dimension_sum, dimension_sum_triangular, gauge_generation_unification, gauge_group_certificate, and gauge_order_product. The gauge_group_certificate theorem assembles the full certificate that B3 forces the ranks (3,2,1) matching the Standard Model; dimension_sum shows the layers sum to the six faces of Q3. In the Recognition framework it realizes the S3 layer of the B3 decomposition that follows from T8 forcing of D=3 and supplies the discrete order 6 that multiplies with the other layers to recover |Aut(Q3)| = 48.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.