dimension_sum

formal source

 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
 280/-- The dimension sum equals D·(D+1)/2 = the D-th triangular number.
 281    For D = 3: T(3) = 6.
 282    The gauge structure exhausts the triangular number of face-pair interactions. -/
 283theorem dimension_sum_triangular :
 284    color_layer.fund_rep_dim + weak_layer.fund_rep_dim + hypercharge_layer.fund_rep_dim
 285    = 3 * (3 + 1) / 2 := by
 286  norm_num [color_layer, weak_layer, hypercharge_layer]
 287
 288/-! ## Part 6: Why Each Layer Maps to Its Gauge Group -/
 289
 290/-- **S₃ → SU(3)**: The permutation group S₃ is the Weyl group of SU(3).
 291
 292    The Weyl group of SU(n) is Sₙ (the symmetric group on n letters).
 293    For n = 3: S₃ acts by permuting the 3 roots of SU(3), which correspond
 294    to the 3 color charges (red, green, blue).
 295
 296    In the cube: S₃ permutes the 3 coordinate axes, which are the 3 face-pairs.
 297    Each face-pair corresponds to one color charge (from QuarkColors). -/
 298theorem s3_is_weyl_of_su3 :
 299    axis_perm_count 3 = Nat.factorial 3 ∧
 300    Nat.factorial 3 = 6 := ⟨rfl, by norm_num⟩
 301
 302/-- **The S₃ Weyl group acts on the same 3 directions as color**.
 303    This is the content of the identification S₃ ↔ SU(3)_color. -/
 304theorem color_from_axis_permutations :
 305    axis_perm_count 3 = Nat.factorial (N_colors 3) := by