cube3_face_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute face counts for any dimension other than three.
- Does not derive the order or full decomposition of the hyperoctahedral group B3.
- Does not connect the face count to mass formulas, constants, or forcing chains.
formal statement (Lean)
120theorem cube3_face_count : cube_face_count 3 = 6 := by
proof body
Term-mode proof.
121 native_decide
122
123/-! ## Part 2: The Hyperoctahedral Group B₃ -/
124
125/-- A signed permutation on D coordinates: a permutation of Fin D together
126 with a sign assignment (each coordinate can be flipped or not).
127
128 This is the hyperoctahedral group B_D, the automorphism group of the
129 D-cube. It acts on ℤ^D by x ↦ (ε₁ · x_{σ(1)}, ..., ε_D · x_{σ(D)})
130 where σ ∈ S_D is the permutation and εᵢ ∈ {±1} are the signs. -/