cube_face_count
plain-language theorem explainer
The definition states that the D-cube has exactly 2D faces. Researchers deriving the Standard Model gauge group from the symmetries of the 3-cube cite this count when decomposing the six faces into three color pairs, two weak couplings, and one hypercharge. It is introduced as a direct arithmetic formula without additional lemmas.
Claim. The number of 2-dimensional faces of the $D$-dimensional hypercube equals $2D$, or equivalently $D$ pairs of opposite faces.
background
In the module deriving the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B₃ of the 3-cube Q₃, this count supplies the total number of faces used to match gauge representation dimensions. The module decomposes B₃ = (ℤ/2ℤ)³ ⋊ S₃, with S₃ acting on the three face-pairs to produce the color structure and the even-sign-flip subgroup (ℤ/2ℤ)² supplying the weak and hypercharge layers. Prior modules already established that the same three face-pairs generate both particle generations and quark colors.
proof idea
The definition is a direct arithmetic expression equating face count to twice the dimension, accompanied by a comment that records the D = 3 case as six faces.
why it matters
This count is invoked by the dimension_sum theorem, which equates the sum of fundamental representation dimensions (3 + 2 + 1) to the face count of Q₃, and by the gauge_group_certificate that confirms the ranks match the cube geometry. It closes the accounting step in P-014 by showing that the total gauge dimension equals the number of faces, completing the unification of color, weak, and hypercharge layers with the cube's combinatorial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.