cube3_vertex_count
plain-language theorem explainer
The declaration establishes that the three-dimensional cube has exactly eight vertices. Researchers deriving Standard Model gauge symmetries from hypercube automorphisms cite this count when enumerating vertices for the 24 chiral fermion flavors in the 3-cube. The proof is a one-line wrapper that reduces directly to the general D-cube vertex formula and evaluates the power numerically.
Claim. The set of vertices of the 3-cube, defined as maps from a 3-element index set to a 2-element set, has cardinality 8.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q₃, building on prior derivations of three generations and three colors from face-pairs. CubeVertex D is the type of functions from Fin D to Fin 2, i.e., the binary coordinate tuples that label the vertices of the D-dimensional hypercube. The general upstream result states that the number of vertices of the D-cube is 2^D, proved by reducing to the cardinality of the function type Fin D → Fin 2.
proof idea
This is a one-line wrapper that applies the general cube_vertex_count theorem for arbitrary D and then invokes norm_num to evaluate 2^3 = 8.
why it matters
This supplies the concrete vertex count for D = 3 that anchors the gauge-group derivation and the 24 chiral fermion flavors (= D × 2^D) listed in the SpectralEmergence structure. It instantiates the D = 3 case fixed by the forcing chain (T8) and feeds the layer decomposition of the hyperoctahedral group B₃ into SU(3) × SU(2) × U(1). No open scaffolding remains for this count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.