hypercharge_layer
plain-language theorem explainer
The hypercharge_layer definition supplies the U(1) component in the gauge structure extracted from the 3-cube automorphism group B3. Physicists reconstructing the Standard Model gauge group from geometric symmetries cite this layer to complete the (3,2,1) rank sequence. It is a direct record definition assigning fundamental representation dimension 1 and discrete order 2 to the parity sign-flip sector.
Claim. The hypercharge layer is the gauge layer with name $U(1)$ hypercharge, fundamental representation dimension 1, and discrete order 2.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3, where B3 = (Z/2Z)^3 ⋊ S3 has order 48 and acts by signed permutations on three axes. The GaugeLayer structure records a name, fundamental representation dimension, and discrete order for each extracted layer; these dimensions match the fundamental representations of the gauge factors (3 for SU(3) from axis permutations, 2 for SU(2) from even sign flips, and 1 for U(1) from parity). This continues earlier derivations of three generations from face-pairs and three colors from the same cube geometry.
proof idea
Direct definition of the GaugeLayer record literal with the three fields set for the hypercharge component.
why it matters
This definition is referenced by cube_gauge_ranks, dimension_sum, dimension_sum_triangular, gauge_order_product, and gauge_group_certificate. The last of these states that the Standard Model gauge group is forced by Q3 symmetries, with the three layers supplying ranks (3,2,1) whose orders multiply to |Aut(Q3)| = 48 and whose dimensions sum to the number of faces. It realizes the P-014 claim that the full gauge structure, not just the SU(3) factor, follows from the hyperoctahedral group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.