spectral_gap_multiplicity_eq_degree
plain-language theorem explainer
The multiplicities of the spectral gap on the cubic lattice Q3 equal the list [1, 3, 3, 1]. Researchers deriving renormalization-group flows on recognition lattices cite this equality to justify the factor of spatial dimension D in anomalous-dimension denominators. The proof is a one-line wrapper that unfolds the two definitions and applies native decision to confirm numerical identity.
Claim. The multiplicity list of the spectral gap for the cubic lattice equals $[1, D, D, 1]$, where $D = 3$ is the spatial dimension.
background
The module treats the integer cubic lattice equipped with unit cell Q3 as the setting for the thermal fixed-point operator. Renormalization proceeds along the phi-ladder forced by self-similarity (T6), whose Fibonacci recurrence yields the characteristic polynomial whose unique positive root is phi. The upstream definition Q3_degree sets the graph degree to 3, while Q3_multiplicities records the binomial coefficients C(3,k) for k = 0 to 3, giving the list [1, 3, 3, 1].
proof idea
The proof is a one-line wrapper that unfolds the definitions of Q3_multiplicities and Q3_degree, then invokes native_decide to verify the numerical equality.
why it matters
This supplies the structural reason why D = 3 appears in the denominator of the anomalous correction. It closes the link between the cubic spectrum and the thermal eigenvalue y_t = phi (hence nu_0 = 1/phi) inside the phi-ladder derivation chain from T6. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.