Q3_eigenvalue_count
plain-language theorem explainer
The theorem states that the Laplacian spectrum of the 3-cube Q3 contains exactly eight eigenvalues, matching its vertex count. Modelers of discrete geometry or graph Laplacians in quantum or gravitational contexts would cite it for basic consistency of spectral data. The proof is a one-line wrapper that unfolds the explicit eigenvalue list and vertex definitions then applies native_decide.
Claim. The length of the list of Laplacian eigenvalues of the three-dimensional hypercube $Q_3$ equals the number of its vertices: length$([0,2,2,2,4,4,4,6])=8$.
background
The CubeSpectrum module formalizes the combinatorial and spectral properties of the 3-cube $Q_3$, the unit cell of $Z^3$, which has 8 vertices, 12 edges, and 6 faces. Its graph Laplacian eigenvalues are given explicitly as the list [0, 2, 2, 2, 4, 4, 4, 6]. Upstream definitions in Constants.AlphaHigherOrder, LambdaRecDerivation, PlanckScaleMatching, and Foundation.SpectralEmergence all set Q3_vertices to 8 (or equivalently $2^3$), with PlanckScaleMatching noting that a curvature packet is distributed over these 8 vertices.
proof idea
This is a one-line wrapper that unfolds the definitions of Q3_laplacian_eigenvalues and Q3_vertices, then applies native_decide to verify that the list has length 8.
why it matters
The result confirms that the supplied spectral data for Q3 is consistent with its vertex count, a prerequisite for using the cube in Recognition Science to model curvature packets and critical exponent corrections. It supports the physical hypotheses in PlanckScaleMatching and the derivations in LambdaRecDerivation that treat Q3 as the basic cell with 8 ticks. No open questions are touched; the declaration is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.