Q3_laplacian_eigenvalues
plain-language theorem explainer
The definition supplies the ordered list of Laplacian eigenvalues for the three-dimensional hypercube graph Q₃ as [0, 2, 2, 2, 4, 4, 4, 6]. Researchers in spectral graph theory within Recognition Science cite it when verifying trace identities or multiplicity counts for the ℤ³ unit cell. The entry is introduced as a direct constant definition with no lemmas or tactics required.
Claim. The Laplacian eigenvalues of the three-cube graph $Q_3$ are the list $[0, 2, 2, 2, 4, 4, 4, 6]$.
background
The module encodes combinatorial and spectral properties of the three-dimensional hypercube $Q_3$, the unit cell of the integer lattice ℤ³. This graph has eight vertices, twelve edges, and six faces, with automorphism group of order 48. The Laplacian spectrum is stated directly with multiplicities one for eigenvalue 0, three for 2, three for 4, and one for 6.
proof idea
Direct definition that hard-codes the known eigenvalue list for the Q₃ graph Laplacian.
why it matters
This supplies the spectral data required by the Q3Cert structure, which encodes the Euler characteristic and trace identity for the critical simplex vertex count of four in three dimensions. It supports the eigenvalue count and trace theorems that feed critical exponent corrections in Recognition Science, consistent with the D = 3 spatial dimensions fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.