modeVariance_ne_zero
plain-language theorem explainer
For Fourier mode k ≥ 1 on an N-site circle with N ≥ 4k, the nonnegative mode variance v_N(k) is strictly positive, so the one-mode Gaussian is non-degenerate (not a Dirac mass). Analysts checking the C10 cylinder-measure preflight cite this as the non-vacuity gate. The proof reduces the NNReal claim to the already-proved positivity of the real inverse eigenvalue via the toNNReal zero criterion.
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 and $v_N(k)=\lambda_N(k)^{-1}$ for the mode variance, packaged in $\mathbb{R}_{\ge 0}$. Then $v_N(k)\ne 0$.
background
This lives in the one-mode cylinder-measure preflight for the QG campaign's C10 bet. The setting is deliberately narrow: a single Fourier mode $k$ on the $N$-site discretization of the unit circle, not a path-sum or field-theoretic measure. No campaign flag is claimed here.
The frozen quadratic energy has discrete Hessian eigenvalue $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ (lattice eigenvalue). Its continuum counterpart is $(2\pi k)^2$. The Boltzmann weight is the centered Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$, stored as a real (modeVarianceReal) and as an $\mathbb{R}_{\ge 0}$ value (modeVariance).
Upstream, latticeEigenvalue_lower_bound gives $\lambda_N(k)\ge(2\pi k)^2/2$ under the same hypotheses $k\ge 1$, $N\ge 4k$, via the Phase-2a sine expansion. That lower bound keeps the inverse controlled and feeds the real positivity lemma used here.
proof idea
One short tactic block. Invoke the sibling positivity theorem for the real variance under the same $(k,N)$ hypotheses. Unfold the $\mathbb{R}_{\ge 0}$ packaging and rewrite nonzero as the negation of the toNNReal zero criterion (equivalently, the real value is not $\le 0$). Discharge by the real positivity fact already in hand. No new spectral estimates are proved at this step.
why it matters
This is Target 4 (non-vacuity) in the one-mode preflight: the cylinder measure $\mu_N$ must be a genuinely non-degenerate Gaussian, not a Dirac mass at zero. Without a nonzero variance parameter, characteristic-function and second-moment statements about gaussianReal would be vacuous for the continuum-limit story.
It sits downstream of the lattice eigenvalue lower bound and the real positivity lemma, and upstream of any rate or weak-convergence claims that treat $\mu_N$ as a proper Gaussian family. The module is Phase 2b SLACK lane M scaffolding toward C10; it carries no flag weight and is separate from the Test G lane. Framework-wise this is ordinary spectral analysis on the circle lattice, not a T0–T8 forcing step, but it is the measure-theoretic hygiene needed before any Recognition gravity continuum limit can be stated honestly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.