cube_edge_count
The definition supplies the standard combinatorial count of edges in a D-dimensional hypercube. Gauge theorists reconstructing the Standard Model group from 3-cube automorphisms cite the formula when enumerating 1-cells of Q3. The implementation is a direct equational definition with no lemmas or tactics.
claimThe number of edges of the $D$-dimensional hypercube is $D · 2^{D-1}$.
background
This definition sits inside the module that derives SU(3) × SU(2) × U(1) from the hyperoctahedral group B3 of the 3-cube Q3. The cube has vertices {0,1}^D; its edges are the 1-cells whose count enters the symmetry analysis. The module builds on prior derivations of three generations from face-pairs and Nc = 3 from the same face-pairs, now extending the count to the full 1-skeleton.
proof idea
The declaration is a definition whose body is the closed-form expression D multiplied by 2 raised to (D-1). No upstream lemmas are invoked; the assignment itself encodes the standard edge-counting rule for the hypercube graph.
why it matters in Recognition Science
The count is used by the downstream theorem cube3_edge_count, which specializes the formula at D = 3 to obtain exactly 12 edges. This supplies the 1-cell enumeration required for the three-layer decomposition of B3 into S3 (SU(3) color) and the even-sign-flip subgroup (SU(2) × U(1)) described in the module documentation. It therefore completes the combinatorial prerequisite for the full gauge-group extraction from cube symmetry.
scope and limits
- Does not apply the formula for non-positive or non-integer D.
- Does not count vertices, faces, or higher cells.
- Does not incorporate the action of the automorphism group on the edges.
- Does not address weighted or embedded realizations of the cube.
Lean usage
theorem cube3_edge_count : cube_edge_count 3 = 12 := by native_decideformal statement (Lean)
109def cube_edge_count (D : ℕ) : ℕ := D * 2 ^ (D - 1)
proof body
Definition body.
110
111/-- For D = 3: 12 edges. -/