Q3_euler
plain-language theorem explainer
The Euler relation for the three-cube asserts that its eight vertices together with its six faces equal its twelve edges plus two. Researchers formalizing the spectral emergence of the cube in Recognition Science cite this identity to anchor the combinatorial counts that enter critical exponent calculations. The proof proceeds as a one-line wrapper that unfolds the three constant definitions and invokes the omega tactic to discharge the resulting arithmetic identity.
Claim. For the three-dimensional hypercube $Q_3$, the number of vertices plus the number of faces equals the number of edges plus two: $8 + 6 = 12 + 2$.
background
The CubeSpectrum module records the combinatorial skeleton of the three-dimensional hypercube $Q_3$ that serves as the unit cell of the integer lattice. The cube is equipped with eight vertices, twelve edges and six faces; its Laplacian spectrum is listed explicitly as the set {0, 2 (multiplicity 3), 4 (multiplicity 3), 6}. These counts appear in upstream derivations of the fine-structure constant corrections and Planck-scale matching.
proof idea
The proof is a one-line wrapper. It unfolds the three constant definitions Q3_vertices, Q3_edges and Q3_faces, then applies the omega tactic to verify the resulting numerical identity 8 + 6 = 12 + 2.
why it matters
This identity is invoked inside the Q3 certificate q3Cert that bundles the vertex, edge, face and Euler data for downstream use in spectral-gap and eigenvalue-count lemmas. It supplies the topological anchor required by the Recognition Science treatment of critical exponent corrections on the cube lattice. The result closes the combinatorial side of the Q3 spectral formalism before the Laplacian eigenvalues are examined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.