dimension_sum_triangular

formal source

 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
 306  simp [axis_perm_count, N_colors, face_pairs]
 307
 308/-- **(ℤ/2ℤ)² → SU(2)**: The even sign-flip subgroup is the Weyl group
 309    of SU(2) × U(1).
 310
 311    SU(2) has Weyl group ℤ/2ℤ (a single reflection).
 312    The (ℤ/2ℤ)² even sign-flip group decomposes as:
 313    - One ℤ/2ℤ for SU(2) (a specific pair-flip)