q3Faces
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.