Q3_spectral_gap
plain-language theorem explainer
The declaration defines the spectral gap of the Q₃ hypercube graph Laplacian as the natural number 2. Researchers modeling critical exponent corrections in Recognition Science cite this constant when forming eigenvalue ratios for the D=3 case. The definition is a direct constant assignment with no computation or lemmas required.
Claim. The spectral gap of the graph Laplacian of the 3-cube $Q_3$ is defined to be the natural number $2$.
background
The module formalizes combinatorial and spectral properties of the 3-dimensional hypercube $Q_3$, the unit cell of $ℤ^3$. It has 8 vertices, 12 edges, 6 faces, and Laplacian eigenvalues {0, 2, 2, 2, 4, 4, 4, 6} with multiplicities {1, 3, 3, 1}. The spectral gap is the smallest positive eigenvalue, fixed here at 2 to match that spectrum.
proof idea
Direct definition that assigns the constant 2, consistent with the listed eigenvalues of the $Q_3$ Laplacian.
why it matters
This supplies the denominator in the downstream theorem Q3_eigenvalue_ratio, which equals the degree and encodes the structural number D + 1 = 4 for D = 3 that appears in the η₁ correction of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.