pith. machine review for the scientific record. sign in
def definition def or abbrev high

hypercharge_layer

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 254def hypercharge_layer : GaugeLayer :=

proof body

Definition body.

 255  { name := "U(1) hypercharge"
 256    fund_rep_dim := 1
 257    discrete_order := 2 }
 258
 259/-- **THEOREM (Gauge Rank Match)**:
 260    The three layers of B₃ have fundamental representation dimensions
 261    (3, 2, 1) — matching the Standard Model gauge group SU(3) × SU(2) × U(1). -/

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.