Q3_eigenvalue_ratio
plain-language theorem explainer
The ratio of the largest Laplacian eigenvalue of the 3-cube to its spectral gap equals the graph degree. Researchers deriving correction-to-scaling factors from lattice spectra in Recognition Science would cite this identity when relating combinatorial degree to eigenvalue spread. The proof is a direct unfolding of the three constant definitions followed by arithmetic simplification.
Claim. Let $Q_3$ be the 3-cube. Let $d$ be its degree, let $g$ be the spectral gap of its graph Laplacian, and let $M$ be the largest eigenvalue. Then $M/g = d$.
background
The module formalizes combinatorial and spectral properties of the 3-cube $Q_3$ (unit cell of $Z^3$) whose Laplacian eigenvalues are {0,2,2,2,4,4,4,6}. The degree is the constant 3, the spectral gap is the smallest positive eigenvalue 2, and the maximum eigenvalue is 6. These constants enter the correction-to-scaling structure, where ratios of consecutive eigenvalues govern subleading RG eigenvalues.
proof idea
The proof is a one-line term that unfolds the definitions of maximum eigenvalue, spectral gap, and degree, then applies the omega tactic to discharge the resulting arithmetic equality.
why it matters
This identity confirms the expected relation for a 3-regular graph on the hypercube and supplies the numerical ratio 3 that appears in scaling analyses. It supports the module's goal of underpinning critical exponent corrections in Recognition Science for the D=3 case. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.