Q3_max_eigenvalue_eq
plain-language theorem explainer
The equality states that the largest Laplacian eigenvalue of the three-dimensional hypercube equals twice its vertex degree. Researchers modeling discrete spacetime lattices cite it to confirm spectral consistency before deriving critical exponent corrections in Recognition Science. The proof is a direct term reduction that expands the two constant definitions and applies arithmetic verification.
Claim. The maximum eigenvalue of the graph Laplacian of the 3-cube satisfies $Q3_max_eigenvalue = 2 * Q3_degree$, where the left side is the constant 6 and the right side is twice the constant degree 3.
background
The module formalizes combinatorial and spectral properties of the 3-cube Q3, the unit cell of the integer lattice Z^3. It records 8 vertices, 12 edges, 6 faces, and the Laplacian spectrum {0, 2, 2, 2, 4, 4, 4, 6} with multiplicities {1, 3, 3, 1}. These facts underpin critical exponent corrections in Recognition Science and link to the D = 3 spatial dimension in the forcing chain.
proof idea
The term proof unfolds the definitions of Q3_max_eigenvalue and Q3_degree to the constants 6 and 3, then applies the omega tactic to discharge the numerical equality 6 = 2 * 3.
why it matters
The result verifies that the Laplacian spectrum of Q3 reaches the upper bound 2d expected for a bipartite regular graph of degree 3. It supplies a basic consistency check inside the CubeSpectrum module that supports later spectral-gap and eigenvalue-count statements used for critical exponents. The equality aligns with the eight-tick octave and D = 3 landmarks of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.