Q3_multiplicities_sum
plain-language theorem explainer
The sum of the eigenvalue multiplicities {1, 3, 3, 1} for the graph Laplacian of the 3-cube equals its vertex count of 8. Researchers deriving critical exponents or curvature corrections in Recognition Science cite this to confirm the spectrum is exhaustive. The proof is a one-line wrapper that unfolds the two constant definitions and lets native_decide evaluate the arithmetic identity.
Claim. The sum of the multiplicities list $[1, 3, 3, 1]$ equals the vertex count of the 3-cube, which is 8.
background
The module formalizes combinatorial and spectral properties of the 3-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_multiplicities is the list [1, 3, 3, 1] identified with binomial coefficients C(3, k). Q3_vertices is the constant 8. Upstream results in AlphaHigherOrder, LambdaRecDerivation, PlanckScaleMatching and SpectralEmergence each record the same vertex count as 8 or 2³, tying the combinatorial fact to the hyperoctahedral automorphism group and curvature-packet axioms.
proof idea
One-line wrapper that unfolds Q3_multiplicities and Q3_vertices then applies native_decide to confirm the numerical sum equals 8.
why it matters
The equality verifies that the listed multiplicities account for every vertex, closing the spectral accounting step required for Laplacian-based corrections in the Recognition Science framework. It directly supports the module's role in supplying the eigenvalue data used by higher-order alpha and lambda derivations. The result sits inside the D = 3 case of the eight-tick octave and the curvature-packet axiom that distributes ±4 curvature over the eight vertices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.