modeVarianceReal_tendsto

This lives in the one-mode cylinder-measure preflight: a toy Mathlib statement about a single Fourier mode on the $N$-site periodic lattice (unit circle, spacing $1/N$). It is not the path-sum measure and carries no campaign flag weight.

The discrete Hessian eigenvalue of the frozen quadratic energy 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 circle. The Boltzmann weight of $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$.

Upstream, modeVarianceReal_rate already gives the quantitative bound $|v_N(k)-(2\pi k)^{-2}|\le(1/6)/N^2$ for $N\ge 4k$. The Phase-2a squeeze lemma states that any sequence obeying $|\mathrm{lam},N-\Lambda|\le C/N^2$ for large $N$ tends to $\Lambda$.

One-line term proof. Instantiate the squeeze lemma eigenvalue_limit_of_uniform_bound on the sequence $N\mapsto v_N(k)$, target $(2\pi k)^{-2}$, rate constant $C=1/6$, and threshold $N_0=4k$. The hypothesis package is exactly the rate theorem modeVarianceReal_rate (valid for $k\ge 1$ and $N\ge 4k$). No further algebraic work.

Qualitative variance convergence is the bridge from the Phase-2a rate to the TARGET-3 statements of the preflight. Downstream, secondMoment_tendsto rewrites the Gaussian second moment $\int x^2,d\mu_N$ as $v_N(k)$ and applies this limit; charFun_modeMeasure_tendsto uses the same limit inside the closed-form characteristic function $\exp(-v_N(k),t^2/2)$ to obtain pointwise char-fun convergence to the continuum Gaussian. Together those feed the panel's live bet C10 (Gaussian cylinder-measure limit over the frozen quadratic energy), still strictly one-mode and still not the path-sum measure.