q3Euler_eq_2
plain-language theorem explainer
The theorem establishes that the Euler characteristic of the 3-cube graph equals 2. Researchers verifying Recognition Science embeddings of canonical lattices would cite this when confirming Q3 is topologically a sphere. The proof is a direct numerical evaluation of the defining expression via the decide tactic.
Claim. For the 3-cube graph, the Euler characteristic satisfies $V - E + F = 2$, where $V$, $E$, and $F$ are the numbers of vertices, edges, and faces.
background
The module develops graph-theoretic consequences of Recognition Science, taking the 3-cube graph Q3 (8 vertices, 12 edges, 6 faces) as the canonical recognition lattice. The Euler characteristic is defined by the sibling declaration q3EulerChar := q3Vertices - q3Edges + q3Faces, which the module states equals the Euler characteristic of the 2-sphere. Upstream results supply the vertex, edge, and face counts that enter this integer expression.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the definition of q3EulerChar, confirming the numerical identity 8 - 12 + 6 = 2.
why it matters
This theorem supplies the euler_q3 field of the downstream graphTheoryDepthCert, which aggregates five canonical theorems to certify configDim D = 5. It directly supports the module claim that Q3 is topologically a sphere and aligns with the Recognition Science forcing chain that derives three spatial dimensions from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.