cube3_face_count
plain-language theorem explainer
The declaration establishes that the three-dimensional cube has exactly six faces by evaluating the general face-count formula at D=3. Researchers deriving the Standard Model gauge group SU(3) × SU(2) × U(1) from the hyperoctahedral symmetry B3 of the 3-cube would cite this count when linking the three face-pairs to color structure and particle generations. The proof reduces to a direct arithmetic evaluation of the definition via native decision.
Claim. The number of faces of the three-dimensional cube equals six, where the face count for dimension $D$ is given by $2D$.
background
The module derives the Standard Model gauge group from the automorphism group B3 of the 3-cube Q3, whose vertices are {0,1}^3. Prior modules established three generations and Nc=3 from the three face-pairs of Q3; this declaration supplies the explicit face count needed to complete the counting layer. The general definition states that the number of faces (2-cells) of the D-cube is 2D, equivalently D pairs of opposite faces each contributing two faces.
proof idea
This is a one-line wrapper that applies native_decide to evaluate the definition cube_face_count at D=3, reducing directly to the arithmetic identity 2*3=6.
why it matters
The result supplies the concrete count of six faces required for the axis-permutation layer S3 in the B3 decomposition, which maps to the Weyl group of SU(3). It closes the counting step in the P-014 derivation of the gauge group from cube symmetry and aligns with the T8 forcing of three spatial dimensions. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.