q3Faces
The definition assigns the constant six to the face count of the three-cube graph. Researchers on Recognition Science lattices cite it when assembling the Euler characteristic that equals two for the sphere topology. It is a direct constant assignment with no computation or lemmas required.
claimThe three-cube graph has six faces: $F(Q_3) = 6$.
background
The module presents Q₃ as the canonical recognition lattice with eight vertices, twelve edges and six faces. The Euler characteristic is defined as V minus E plus F and equals two, matching χ(S²). This structure encodes five canonical graph theorems corresponding to configDim D = 5.
proof idea
This is a direct definition that assigns the constant six to the face count.
why it matters in Recognition Science
It supplies the face count for the downstream Euler characteristic computation that yields two. The definition supports the zero-sorry verification that Q₃ realizes the five graph theorems in the Recognition Science framework.
scope and limits
- Does not derive the face count from graph axioms.
- Does not extend to higher-dimensional hypercubes.
- Does not address chromatic number or other invariants.
Lean usage
def q3EulerChar : ℤ := q3Vertices - q3Edges + q3Facesformal statement (Lean)
31def q3Faces : ℕ := 6