Q3_multiplicities_are_binomial
plain-language theorem explainer
The eigenvalue multiplicities of the Laplacian on the 3-cube graph Q3 equal the binomial coefficients C(3,k) for k=0 to 3. Researchers modeling lattice spectra within Recognition Science cite this to anchor the observed pattern 1,3,3,1 in combinatorial structure. The proof is a one-line unfolding of the multiplicity definition followed by native decision.
Claim. The multiplicity list for the eigenvalues of the graph Laplacian on the 3-cube equals $[{3 choose 0}, {3 choose 1}, {3 choose 2}, {3 choose 3}]$.
background
The module formalizes combinatorial and spectral properties of the 3-dimensional hypercube Q3, the unit cell of Z^3. This graph has 8 vertices, 12 edges and 6 faces; its Laplacian eigenvalues are {0,2,2,2,4,4,4,6} with multiplicities {1,3,3,1}. The sibling definition Q3_multiplicities supplies the concrete list [1,3,3,1] that the theorem identifies with the binomial coefficients.
proof idea
The proof unfolds the definition of Q3_multiplicities and applies native_decide to confirm numerical equality with the binomial list.
why it matters
This theorem verifies the binomial origin of the multiplicity pattern stated in the module documentation, which underpins critical exponent corrections in Recognition Science. It closes the combinatorial check for the D=3 case inside the CubeSpectrum formalization. No downstream results depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.