latticeEigenvalue
plain-language theorem explainer
Defines the discrete Hessian eigenvalue λ_N(k) = 4 N² sin²(π k / N) for Fourier mode k on an N-site periodic lattice (unit circle, spacing 1/N). Anyone working the one-mode Gaussian cylinder preflight or the spectral continuum limit cites this as the frozen quadratic energy scale. It is a pure closed-form definition, not a proved claim.
Claim. For natural numbers $k$ and $N$, the discrete Hessian eigenvalue of Fourier mode $k$ on the $N$-site periodic lattice (in lattice units) is $\lambda_N(k) := 4 N^2 \sin^2(\pi k / N)$.
background
The module is a one-mode toy preflight for panel bet C10: a Gaussian cylinder-measure limit over a frozen quadratic energy. It is not the path-sum measure and carries no campaign flag weight. The lattice is the $N$-site discretization of the unit circle with spacing $1/N$.
For mode $k \ge 1$, the frozen quadratic energy has discrete Hessian eigenvalue $\lambda_N(k)$ in lattice units. The continuum counterpart is $\Lambda(k) = (2\pi k)^2$, the $-d^2/dx^2$ eigenvalue of $e^{2\pi i k x}$ on the unit circle. The Boltzmann weight of $\tfrac12 \lambda x^2$ is then the centered Gaussian of variance $v_N(k) = \lambda_N(k)^{-1}$.
The quantitative continuum expansion $|\lambda_N(k) - (2\pi k)^2| \le ((2\pi k)^4/12)/N^2$ is already proved in SpectralConvergence.discrete_sine_eigenvalue_expansion; this definition simply names the exact discrete side of that identity.
proof idea
No proof: a four-line closed-form definition. The body is the standard second-difference (discrete Laplacian) eigenvalue $4 N^2 \sin^2(\pi k/N)$ on the periodic $N$-cycle, written in lattice units so that the continuum limit is $(2\pi k)^2$ rather than $4\sin^2(\pi k/N)$.
why it matters
This is the fixed a-priori normalization for the entire one-mode cylinder preflight. Downstream, nonnegativity is immediate, and under $k \ge 1$, $N \ge 4k$ one gets the strict positivity and the eventual lower bound $\lambda_N(k) \ge (2\pi k)^2/2$ from the Phase-2a sine expansion. Those feed the mode variance $v_N(k) = \lambda_N(k)^{-1}$ and the TARGET 2 rate $|v_N(k) - (2\pi k)^{-2}| \le (1/6)/N^2$, which keeps the Gaussian cylinder measure under quantitative control as $N \to \infty$.
In the broader QG campaign this is scaffolding for C10 only: a single Fourier mode on a 1D lattice, separate from Test G and from any full path-sum construction. It does not touch the T0–T8 forcing chain, RCL, or the phi-ladder mass formula; it is pure spectral analysis of the frozen quadratic energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.