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

cube3_edge_count

show as:
view Lean formalization →

The three-dimensional cube has exactly 12 edges. Researchers deriving the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of Q3 cite this count when enumerating the edges that arise from the signed-permutation action on three axes. The proof evaluates the closed-form expression D · 2^(D-1) at D = 3 by direct arithmetic reduction.

claimThe edge count of the D-cube is given by $D · 2^{D-1}$, hence the three-dimensional cube has $3 · 2^{2} = 12$ edges.

background

The module derives the full Standard Model gauge group from the hyperoctahedral group B3 of the 3-cube Q3, whose vertices are {0,1}^3 and whose automorphisms are signed permutations of the three axes. The general edge-count function is defined as D · 2^(D-1), which counts each of the D coordinate directions paired with the 2^(D-1) choices of fixed coordinates on the remaining axes. Upstream results supply the J-cost structures and the spectral emergence that simultaneously forces the gauge content (sector dimensions 3 + 2 + 1), three generations, and |Aut(Q3)| = 48 from the same cube geometry.

proof idea

One-line wrapper that applies native_decide to evaluate the arithmetic expression D · 2^(D-1) at D = 3.

why it matters in Recognition Science

This supplies the concrete numerical value required for the D = 3 case in the layer decomposition of B3 = (Z/2Z)^3 ⋊ S3 that yields the Weyl groups of SU(3) and SU(2) × U(1). It directly supports the module's claim that the 3-cube forces the full gauge group together with 24 chiral fermions, closing the gap left by earlier derivations of only the SU(3) factor. The result aligns with the T8 forcing of three spatial dimensions and the eight-tick octave structure.

scope and limits

formal statement (Lean)

 112theorem cube3_edge_count : cube_edge_count 3 = 12 := by

proof body

Term-mode proof.

 113  native_decide
 114
 115/-- Number of faces (2-cells) of the D-cube: 2D.
 116    Equivalently: D pairs of opposite faces, each pair contributing 2 faces. -/

depends on (6)

Lean names referenced from this declaration's body.