Q3_multiplicities_are_binomial
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute or prove the Laplacian eigenvalues themselves.
- Does not generalize the multiplicity formula to hypercubes of dimension other than 3.
- Does not derive the list from graph-theoretic axioms without computation.
- Does not address the automorphism group or its order.
formal statement (Lean)
65theorem Q3_multiplicities_are_binomial :
66 Q3_multiplicities = [Nat.choose 3 0, Nat.choose 3 1, Nat.choose 3 2, Nat.choose 3 3] := by
proof body
Term-mode proof.
67 unfold Q3_multiplicities; native_decide
68
69/-! ## Automorphism Group -/
70
71/-- |Aut(Q₃)| = 48 = |S₃| · |ℤ₂|³ · ... = 2³ · 3! = 8 · 6 = 48.
72 More precisely, Aut(Q_D) = S_D ⋊ ℤ₂^D, order D! · 2^D. -/