cube_vertex_count
plain-language theorem explainer
The declaration states that the D-dimensional hypercube has exactly 2^D vertices, identified with all functions from a D-element set to a two-element set. Researchers deriving the hyperoctahedral symmetry of the 3-cube for the Standard Model gauge group cite this count to fix the vertex set size before decomposing the automorphism group. The proof is a one-line wrapper that reduces directly to the cardinality of the function type Fin D → Fin 2.
Claim. The set of all functions from a finite set of cardinality D to a two-element set has cardinality $2^D$.
background
The GaugeFromCube module derives SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q₃. Vertices of the D-cube are defined as functions from Fin D to Fin 2, equipped with the natural Fintype instance for function types. This supplies the base count needed to specialize to D = 3 and obtain the eight vertices that generate the (ℤ/2ℤ)^3 factor in the hyperoctahedral group B₃ = (ℤ/2ℤ)^3 ⋊ S₃.
proof idea
The proof is a one-line wrapper that applies Fintype.card_fun to the function type Fin D → Fin 2 after unfolding the definition of CubeVertex via simpa.
why it matters
This result is invoked by the downstream specialization cube3_vertex_count to obtain eight vertices for the 3-cube. It anchors the vertex counting step in the module's three-layer decomposition of B₃, where the eight vertices correspond to the sign-flip subgroup that contributes the SU(2) × U(1) structure, as described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.