Q3_vertices_eq
plain-language theorem explainer
The equality asserts that the vertex count of the three-dimensional hypercube equals two raised to the graph degree. Researchers deriving the Laplacian spectrum for Recognition Science models cite this identity to anchor the eigenvalue multiplicities. The proof reduces directly to unfolding the two constant definitions and resolving the arithmetic equality.
Claim. The vertex count of the three-dimensional hypercube graph equals two raised to its degree: $8 = 2^3$.
background
The module formalizes combinatorial and spectral properties of the three-dimensional hypercube Q₃, the unit cell of ℤ³, whose graph Laplacian has eigenvalues {0, 2, 2, 2, 4, 4, 4, 6} with multiplicities {1, 3, 3, 1}. Q3_vertices is defined as the natural number 8 and Q3_degree as the natural number 3. Upstream definitions in Constants.AlphaHigherOrder and LambdaRecDerivation likewise fix the vertex count at 8, supplying the base count used for spectral derivations.
proof idea
The proof is a one-line wrapper that unfolds Q3_vertices and Q3_degree, then applies the omega tactic to discharge the resulting arithmetic statement.
why it matters
This identity anchors the spectral analysis of Q₃ that underpins critical exponent corrections in Recognition Science. It feeds the theorem Q3_vertices_eq in Constants.AlphaHigherOrder, which directly records the vertex count as 8. The result connects to the Recognition framework by supplying the combinatorial foundation for the Laplacian spectrum that determines eigenvalue structure for higher-order constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.