q3EulerChar
plain-language theorem explainer
This definition computes the Euler characteristic of the 3-cube graph Q3 as the integer V minus E plus F using the fixed counts for that graph. Researchers in Recognition Science graph theory cite it to confirm that Q3 matches the topology of a sphere. It arises as a direct arithmetic expression combining the vertex, edge, and face numbers supplied by sibling definitions.
Claim. Let $Q_3$ denote the three-dimensional cube graph. Its Euler characteristic is defined by the expression $V - E + F$, where $V$, $E$, and $F$ are the numbers of vertices, edges, and faces of $Q_3$.
background
The module establishes Q3 as the canonical recognition lattice in Recognition Science, with eight vertices, twelve edges, and six faces. The Euler characteristic formula V - E + F is applied directly to these counts. Upstream results define the vertex count as two to the power three, the edge count as three times two to the power two, and the face count as six, enabling the computation that yields two and matches the Euler characteristic of the two-sphere.
proof idea
The definition is a one-line arithmetic combination that subtracts the edge count from the vertex count and then adds the face count.
why it matters
It provides the Euler characteristic component for the GraphTheoryDepthCert structure, which asserts that five graph theorems hold and that the Q3 Euler characteristic equals two. This supports the framework identification of Q3 with the sphere topology and the assignment of five theorems to configDim D equals five. The downstream result that proves the Euler characteristic equals two then discharges the numerical claim by direct evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.