CubeVertex
plain-language theorem explainer
Vertices of the D-cube are maps from D axes to binary values. Researchers deriving SU(3) × SU(2) × U(1) from the 3-cube automorphism group cite this to obtain the 8 vertices and their signed-permutation action. The declaration is a one-line type abbreviation that inherits Fintype and DecidableEq from function spaces.
Claim. The vertices of the $D$-cube are the functions from a set of $D$ elements to the set with two elements.
background
Module P-014 derives the full Standard Model gauge group from the automorphism group of the 3-cube Q₃. A vertex is formalized as an assignment of 0 or 1 to each coordinate axis, supplying the domain on which the hyperoctahedral group B₃ = (ℤ/2ℤ)³ ⋊ S₃ acts by signed permutations. This supports the three-layer decomposition: axis permutations (S₃) for the SU(3) color structure, even sign flips for the SU(2) × U(1) Weyl group, and the full order-48 group for the combined gauge content. Upstream, SpectralEmergence.of structures how Q₃ simultaneously forces gauge dimensions 3+2+1, three generations from face-pairs, and 24 chiral fermions (= D × 2^D).
proof idea
The declaration is a one-line type abbreviation. It is followed by two instances that delegate Fintype and DecidableEq directly to the corresponding instances on Fin D → Fin 2.
why it matters
This supplies the vertex set whose cardinality and symmetry generate the gauge group in the Recognition framework. It is used by cube_vertex_count (which proves 2^D vertices) and cube3_vertex_count (which specializes to 8 vertices). The definition anchors the B₃ decomposition that produces the Weyl groups for SU(3), SU(2) and U(1) as described in the module doc-comment. It touches the open embedding question of how the discrete hyperoctahedral action lifts to the continuous gauge group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.