latticeEigenvalue_lower_bound
plain-language theorem explainer
For Fourier mode k ≥ 1 on an N-site circle with N ≥ 4k, the discrete Hessian eigenvalue λ_N(k) is at least half the continuum value (2πk)². Anyone controlling one-mode Gaussian variances or inverse-eigenvalue rates in the cylinder preflight cites this bound. The proof feeds the Phase-2a sine expansion into elementary π ≤ 4 comparisons that absorb the O(1/N²) error.
Claim. Let $k,N\in\mathbb{N}$ with $k\ge 1$ and $N\ge 4k$. Write $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ for the discrete Hessian eigenvalue of mode $k$ and $\Lambda(k)=(2\pi k)^2$ for the continuum $-d^2/dx^2$ eigenvalue on the unit circle. Then $\Lambda(k)/2\le\lambda_N(k)$.
background
This lives in the one-mode cylinder-measure preflight (QG Phase 2b SLACK lane M): a Mathlib-only toy about a single Fourier mode on the $N$-site discretization of the unit circle, not the path-sum measure and carrying no campaign flag weight.
The discrete Hessian eigenvalue in lattice units is $\lambda_N(k)=4N^2\sin^2(\pi k/N)$. Its continuum counterpart is $\Lambda(k)=(2\pi k)^2$, the $-d^2/dx^2$ eigenvalue of $e^{2\pi i kx}$ on the unit-length circle. The frozen quadratic energy $\tfrac12\lambda x^2$ has Boltzmann weight the centered Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$.
The quantitative continuum limit is already proved upstream as discrete_sine_eigenvalue_expansion: $|\lambda_N(k)-\Lambda(k)|\le((2\pi k)^4/12)/N^2$. The present bound turns that two-sided expansion into a one-sided floor $\lambda_N\ge\Lambda/2$ once $N$ is large enough relative to $k$, so that inverses stay controlled.
proof idea
Invoke discrete_sine_eigenvalue_expansion to get $|\lambda_N-\Lambda|\le((2\pi k)^4/12)/N^2$, hence $\lambda_N\ge\Lambda-((2\pi k)^4/12)/N^2$. It remains to show the error term is at most $\Lambda/2$.
Cast $k\ge 1$ and $N\ge 4k$ to reals. From $\pi\le 4$ one gets $\pi^2\le 16$, and with $N\ge 4k$ one obtains $(2\pi k)^2\le 6N^2$. Clearing denominators then yields $((2\pi k)^4/12)/N^2\le(2\pi k)^2/2$. Unfold both eigenvalue defs and finish by linarith on the lower half of the absolute-value expansion plus this key comparison.
why it matters
Without a uniform floor on $\lambda_N$, the mode variance $v_N=\lambda_N^{-1}$ can blow up and the Gaussian cylinder measure becomes degenerate. This bound is the denominator control used by modeVarianceReal_rate (TARGET 2): $|v_N-\Lambda^{-1}|\le(1/6)/N^2$, via $|\Lambda-\lambda|/(\lambda\Lambda)\le(\Lambda^2/12/N^2)/(\Lambda^2/2)$.
It also feeds latticeEigenvalue_pos (strict positivity in scope) and thereby modeVariance_ne_zero (NON-VACUITY target 4: the Gaussian is not Dirac). In the broader Recognition gravity campaign this is preflight bookkeeping for candidate C10, not a forcing-chain step (T0–T8) and not a claim about the full path-sum measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.