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 three-layer decomposition of the 3-cube automorphism group B3. Gauge theorists deriving the Standard Model group from discrete geometry cite it to complete the (3,2,1) rank triple. It is a direct record construction assigning fundamental representation dimension 1 and discrete order 2.

claimThe hypercharge gauge layer is the record with name ``U(1) hypercharge'', fundamental representation dimension 1, and discrete order 2.

background

The GaugeLayer structure records the name, fundamental representation dimension, and discrete order for each gauge component. In this module the 3-cube Q3 has automorphism group B3 of order 48, which decomposes into axis permutations S3 (color, dimension 3), even sign flips of order 4 (weak, dimension 2), and the remaining parity factor (hypercharge, dimension 1). The module builds on prior derivations of three generations from face-pairs and three colors from the same geometry.

proof idea

This is a definition that directly constructs the GaugeLayer record with the three fields set to the hypercharge values. No lemmas or tactics are invoked; the assignment completes the layer triple used by downstream rank and order calculations.

why it matters in Recognition Science

The definition supplies the missing U(1) entry required by gauge_group_certificate, dimension_sum, and gauge_order_product. Those theorems establish that the ranks (3,2,1) and orders (6,4,2) reproduce the Standard Model group and the order of B3. Within Recognition Science this realizes the D=3 triangular decomposition 3+2+1=6 of face-pair interactions.

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.