weak_layer
plain-language theorem explainer
The weak_layer definition specifies the SU(2) weak gauge structure extracted from the even sign-flip subgroup of the 3-cube automorphism group B3, recording fundamental representation dimension 2 and discrete order 4. Physicists assembling geometric derivations of the Standard Model gauge group from Q3 symmetry cite this when forming the (3,2,1) rank tuple. It is a direct record construction of the GaugeLayer structure with no lemmas or reductions applied.
Claim. The weak gauge layer is the GaugeLayer record with name ``SU(2) weak'', fundamental representation dimension $2$, and discrete order $4$.
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, where B3 = (Z/2Z)^3 ⋊ S3 has order 48. The GaugeLayer structure records a name, fundamental representation dimension (corresponding to the dimension of the fundamental representation of the associated Lie group), and discrete order for each layer. The module decomposes B3 into three layers: axis permutations S3 (order 6, dimension 3) for color, even sign flips (Z/2Z)^2 (order 4, dimension 2) for weak isospin, and the remaining parity for hypercharge (dimension 1). This builds directly on the GaugeLayer definition and the cube symmetry facts imported from DimensionForcing and ParticleGenerations.
proof idea
The definition is a direct record construction that populates the three fields of GaugeLayer with the fixed values name := ``SU(2) weak'', fund_rep_dim := 2, and discrete_order := 4. No lemmas are invoked and no tactics are used; the body is a pure data literal.
why it matters
This supplies the middle component of the gauge rank tuple used in cube_gauge_ranks and the dimension sum theorem (which equals the number of faces of Q3). It feeds the gauge_group_certificate establishing that B3 forces the full SM gauge group ranks (3,2,1) and the gauge_order_product showing the product of discrete orders recovers |Aut(Q3)| = 48. In the Recognition framework it completes the mapping from the T8 D = 3 spatial dimensions and the eight-tick octave structure to the weak layer via the even sign-flip subgroup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.