 246    fund_rep_dim := 3
 247    discrete_order := 6 }
 248
 249def weak_layer : GaugeLayer :=
 250  { name := "SU(2) weak"
 251    fund_rep_dim := 2
 252    discrete_order := 4 }
 253
 254def hypercharge_layer : GaugeLayer :=
 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). -/
 262theorem gauge_rank_match :
 263    color_layer.fund_rep_dim = 3 ∧
 264    weak_layer.fund_rep_dim = 2 ∧
 265    hypercharge_layer.fund_rep_dim = 1 := ⟨rfl, rfl, rfl⟩
 266
 267/-- **THEOREM (Dimension Sum)**:
 268    The fundamental representation dimensions sum to the number of
 269    cube face-pairs (= D = 3) PLUS the number of face-pair COUPLINGS.
 270
 271    3 + 2 + 1 = 6 = number of faces of Q₃
 272
 273    This is not a coincidence: the 6 faces of the cube decompose as
 274    3 face-pairs (color) + 2 face-pair couplings (weak) + 1 parity (hypercharge). -/
 275theorem dimension_sum :
 276    color_layer.fund_rep_dim + weak_layer.fund_rep_dim + hypercharge_layer.fund_rep_dim
 277    = cube_face_count 3 := by
 278  native_decide
 279

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.