weak_layer
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the continuous Lie group structure or representation theory of SU(2).
- Does not derive coupling constants, particle masses, or interaction vertices.
- Does not address unification with gravity or other forces beyond the gauge group.
- Does not prove uniqueness of the layer assignment among possible group decompositions.
formal statement (Lean)
249def weak_layer : GaugeLayer :=
proof body
Definition body.
250 { name := "SU(2) weak"
251 fund_rep_dim := 2
252 discrete_order := 4 }
253