Q3_multiplicities
plain-language theorem explainer
The definition supplies the eigenvalue multiplicities [1, 3, 3, 1] for the Laplacian of the three-dimensional hypercube graph Q3. Lattice physicists and Recognition Science researchers cite it when extracting the structural factor D = 3 that enters anomalous-dimension denominators. It is a direct constant definition that matches the binomial coefficients C(3, k) for k = 0 to 3.
Claim. The multiplicities of the eigenvalues of the graph Laplacian on the 3-cube are the list $[1, 3, 3, 1]$, which equals the binomial coefficients $[C(3,0), C(3,1), C(3,2), C(3,3)]$.
background
The module Q3 Cube Spectral Formalism treats the 3-dimensional hypercube Q3 as the unit cell of the integer lattice Z^3. This graph has 8 vertices, 12 edges and 6 faces; its Laplacian spectrum consists of the values 0, 2, 2, 2, 4, 4, 4, 6 whose multiplicities are exactly the list supplied by the definition. The same multiplicities appear in the Recognition Science derivation of critical-exponent corrections because they encode the degeneracy of the spectral gap.
proof idea
The declaration is a direct definition that hard-codes the list [1, 3, 3, 1]. Subsequent theorems simply unfold the identifier and apply native_decide to obtain the binomial and sum identities.
why it matters
The definition is the combinatorial input for Q3_multiplicities_are_binomial, Q3_multiplicities_sum and the theorem spectral_gap_multiplicity_eq_degree. The last result states that the gap multiplicity equals the graph degree D = 3, supplying the structural reason D appears in the denominator of the anomalous correction. This step is required by the T8 forcing of three spatial dimensions and the eight-tick octave in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.