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

dimension_sum

show as:
view Lean formalization →

The fundamental representation dimensions of the color, weak, and hypercharge layers extracted from the hyperoctahedral group B3 sum exactly to the face count of the 3-cube. Researchers deriving the Standard Model gauge group from geometric symmetries would cite this equality to close the dimensional accounting. The proof is a direct numerical evaluation that confirms 3 + 2 + 1 equals 6.

claimLet $d_c$, $d_w$, $d_h$ be the fundamental representation dimensions of the color, weak, and hypercharge layers. Then $d_c + d_w + d_h = 6$, where 6 equals the number of faces of the three-dimensional cube.

background

The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3, whose elements are signed permutations of three axes. GaugeLayer is a structure recording a name, fund_rep_dim, and discrete_order for each layer. color_layer sets fund_rep_dim to 3 from axis permutations, weak_layer sets it to 2 from even sign flips, and hypercharge_layer sets it to 1 from parity. cube_face_count D is defined as 2D, so the case D = 3 yields 6 faces.

proof idea

The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic identity 3 + 2 + 1 = 6.

why it matters in Recognition Science

This theorem closes the dimensional sum in the module's derivation of the gauge group from cube symmetry, confirming that the three layers exhaust the six faces of Q3 as 3 face-pairs plus 2 couplings plus 1 parity. It directly supports the module claim that the decomposition is not coincidental. No downstream uses are recorded yet.

scope and limits

formal statement (Lean)

 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

proof body

Term-mode proof.

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

depends on (12)

Lean names referenced from this declaration's body.