limitVariance_pos
plain-language theorem explainer
For every Fourier mode k ≥ 1, the continuum limiting variance (2πk)^{-2} is strictly positive. Citers of the one-mode cylinder Gaussian preflight need this to guarantee the limit object is a non-degenerate Gaussian, not a Dirac mass. The proof unfolds the continuum eigenvalue (2πk)², gets positivity from π and k, then inverts.
Claim. For every natural number $k \ge 1$, writing $\lambda_\infty(k) = (2\pi k)^2$ for the continuum eigenvalue of mode $k$ on the unit circle, one has $0 < \lambda_\infty(k)^{-1}$. Equivalently the limiting one-mode variance $(2\pi k)^{-2}$ is strictly positive.
background
This lives in the one-mode cylinder-measure preflight for the QG campaign's live bet C10: a Gaussian cylinder-measure limit over a frozen quadratic energy. The module is deliberately a toy for a single Fourier mode $k$ on a one-dimensional periodic lattice. It is not the path-sum measure, carries no campaign flag weight, and is separate from the Test G lane.
The lattice is the $N$-site discretization of the unit circle. For mode $k \ge 1$ the discrete Hessian eigenvalue is $\lambda_N(k) = 4 N^2 \sin^2(\pi k/N)$, with continuum limit $\lambda_\infty(k) = (2\pi k)^2$, the $-d^2/dx^2$ eigenvalue of $e^{2\pi i k x}$ on the unit-length circle. The Boltzmann weight of the frozen quadratic $\tfrac12 \lambda x^2$ is the centered Gaussian of variance $v_N(k) = \lambda_N(k)^{-1}$.
The continuum eigenvalue is defined exactly as $(2\pi k)^2$. The limiting variance is therefore its reciprocal $(2\pi k)^{-2}$. TARGET 4 of the preflight asks that this variance be strictly positive so the limit Gaussian is non-degenerate.
proof idea
Cast $1 \le k$ to the reals. Unfold the continuum eigenvalue to $(2\pi k)^2$. The product $2\pi k$ is positive because $\pi > 0$ and $k \ge 1$ (via nlinarith and Real.pi_pos), so the square is positive by positivity. Apply inv_pos to conclude the reciprocal is positive.
why it matters
TARGET 4 (J ≠ 0) in the C10 one-mode preflight: without a strictly positive limiting variance the continuum object would collapse to a point mass and the Gaussian cylinder story would be vacuous. The module header stresses that everything here is a genuine Mathlib statement about ProbabilityTheory.gaussianReal, with no sorry and no new axioms.
No downstream theorem currently depends on this declaration (used_by is empty); it is a local positivity gate inside the preflight, sitting beside nonnegativity of the lattice eigenvalue, the mode variance packaging, and the characteristic-function / second-moment facts for the one-mode measure. In the broader Recognition gravity analysis it supports the claim that the frozen quadratic energy yields a well-defined non-degenerate Gaussian mode in the continuum limit, a necessary bookkeeping step before any multi-mode or path-sum construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.