pith. machine review for the scientific record. sign in
theorem proved term proof high

dimension_sum_triangular

show as:
view Lean formalization →

The sum of the fundamental representation dimensions of the color, weak, and hypercharge layers extracted from the 3-cube automorphism group equals the third triangular number 6. A physicist reconstructing the Standard Model gauge structure from hyperoctahedral symmetry B3 would cite this to confirm the layer dimensions exhaust the triangular count of face-pair interactions. The proof is a direct numerical substitution of the layer constants.

claimLet the three gauge layers be extracted from the automorphism group of the 3-cube. Then the sum of their fundamental representation dimensions satisfies $3 + 2 + 1 = 6$, which equals the third triangular number $D(D+1)/2$ for $D=3$.

background

The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the hyperoctahedral group B3 of the 3-cube Q3, whose vertices are {0,1}^3 and whose order is 48. B3 decomposes into three layers: axis permutations S3 (order 6) for color, even sign flips (Z/2Z)^2 (order 4) for weak, and the remaining sign structure for hypercharge. The referenced layer definitions assign fund_rep_dim values 3, 2, and 1 respectively, matching the Weyl groups of the corresponding factors. Upstream results supply the discrete structures for nuclear densities and J-calibration that frame the overall Recognition Science derivation of gauge structure from cube symmetry.

proof idea

The proof is a one-line wrapper that applies norm_num to the three layer definitions, substituting the constants fund_rep_dim := 3, 2, 1 directly into the left-hand side and reducing the right-hand side 3*(3+1)/2 to 6.

why it matters in Recognition Science

This equality verifies that the three layers from B3 = (Z/2Z)^3 ⋊ S3 together saturate the triangular number T(3) = 6 of face-pair interactions required by D = 3 spatial dimensions in the forcing chain. It closes the dimension count in the module's derivation of the full gauge group from cube symmetry, linking the S3 Weyl action to SU(3) color and the even-sign subgroup to SU(2) × U(1). No downstream theorems are recorded yet.

scope and limits

formal statement (Lean)

 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

proof body

Term-mode proof.

 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). -/

depends on (17)

Lean names referenced from this declaration's body.