modeVarianceReal_rate
plain-language theorem explainer
For each Fourier mode k ≥ 1 on an N-site circle with N ≥ 4k, the one-mode Gaussian variance v_N(k) = λ_N(k)^{-1} approximates the continuum value (2πk)^{-2} at rate at most (1/6) N^{-2}, with C = 1/6 independent of k. Anyone citing the cylinder-measure preflight or the variance limit uses this quantitative bound. The proof divides the Phase-2a eigenvalue expansion by a lower bound λΛ ≥ Λ²/2 and simplifies.
Claim. Let $k \ge 1$ and $N \ge 4k$ be natural numbers. Write $\lambda_N(k) = 4N^2 \sin^2(\pi k/N)$ for the discrete Hessian eigenvalue and $\Lambda(k) = (2\pi k)^2$ for the continuum eigenvalue. Then $\bigl|\lambda_N(k)^{-1} - \Lambda(k)^{-1}\bigr| \le \frac{1}{6}\, N^{-2}$.
background
This lives in the one-mode cylinder-measure preflight: a toy Mathlib analysis of a single Fourier mode on the $N$-site discretization of the unit circle, not the path-sum or any field-theoretic measure. The discrete Hessian eigenvalue is $\lambda_N(k) = 4N^2\sin^2(\pi k/N)$; the continuum counterpart is $\Lambda(k)=(2\pi k)^2$, the $-d^2/dx^2$ eigenvalue of $e^{2\pi i kx}$. The Boltzmann weight of the frozen quadratic energy $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$.
Phase 2a already supplies the quantitative continuum limit $|\lambda_N(k)-\Lambda(k)|\le(\Lambda(k)^2/12)/N^2$ via discrete_sine_eigenvalue_expansion, and a matching lower bound $\lambda_N(k)\ge\Lambda(k)/2$ under $N\ge 4k$. The present statement lifts that eigenvalue control to the inverse (the variance).
proof idea
Cast the hypotheses to $\mathbb{R}$ and record positivity of $N$, $\Lambda$, and $\lambda$. For the numerator, commute the absolute difference and rewrite $\Lambda^2=(2\pi k)^4$, then apply discrete_sine_eigenvalue_expansion to get $|\Lambda-\lambda|\le\Lambda^2/(12N^2)$. For the denominator, multiply the lattice lower bound by $\Lambda>0$ to obtain $\lambda\Lambda\ge\Lambda^2/2$. Use the algebraic identity $\lambda^{-1}-\Lambda^{-1}=(\Lambda-\lambda)/(\lambda\Lambda)$, take absolute values, and bound the quotient by dividing the numerator estimate by the denominator lower bound. The resulting fraction simplifies by field arithmetic to $(1/6)N^{-2}$.
why it matters
This is Target 2 of the one-mode preflight: the uniform-in-$k$ rate that feeds the variance limit. Downstream, modeVarianceReal_tendsto composes it with the Phase-2a squeeze eigenvalue_limit_of_uniform_bound to conclude $v_N(k)\to(2\pi k)^{-2}$ as $N\to\infty$. That limit is the quantitative backbone for the Gaussian cylinder-measure statements later in the same module (characteristic function, second moment, measure convergence formulations).
In the broader QG campaign this is Phase 2b SLACK lane M material: genuine Mathlib analysis with no sorry and no flag weight. It does not touch the Recognition forcing chain (T0–T8), RCL, or the mass ladder; it only prepares the spectral side of a frozen quadratic energy on a circle. The open question it supports is whether the one-mode Gaussian picture can later be upgraded toward panel bet C10, still without claiming that upgrade here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.