modeVarianceReal_pos
plain-language theorem explainer
Under k ≥ 1 and N ≥ 4k, the one-mode lattice Gaussian variance v_N(k) = λ_N(k)^{-1} is strictly positive, so the mode is non-degenerate. Cited by anyone checking non-vacuity of the one-mode cylinder-measure preflight. Proof is a one-line reciprocal of the already-proved lattice-eigenvalue positivity.
Claim. For $k,N\in\mathbb{N}$ with $k\ge 1$ and $N\ge 4k$, the one-mode variance $v_N(k):=\lambda_N(k)^{-1}$ satisfies $0<v_N(k)$, where $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ is the discrete Hessian eigenvalue of the frozen quadratic energy on the $N$-site periodic lattice.
background
This module is a one-mode toy preflight for panel bet C10: a Gaussian cylinder-measure limit over a frozen quadratic energy. It treats a single Fourier mode $k$ on the $N$-site discretization of the unit circle (spacing $1/N$). It is not the path-sum measure, constructs no field-theoretic measure, and flips no campaign flag.
The discrete Hessian eigenvalue in lattice units is $\lambda_N(k):=4N^2\sin^2(\pi k/N)$. Its continuum counterpart is $(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}$ (junk value $0$ when the eigenvalue vanishes, by $0^{-1}=0$).
Upstream, lattice-eigenvalue positivity already gives $0<\lambda_N(k)$ whenever $k\ge 1$ and $N\ge 4k$, via positivity of the continuum eigenvalue and the discrete-to-continuum comparison.
proof idea
Term-mode one-liner. The variance is defined as the reciprocal of the lattice eigenvalue, so Mathlib's inv_pos converts eigenvalue positivity into variance positivity. The proof is exactly inv_pos.mpr applied to latticeEigenvalue_pos at the same $(k,N)$ and the same scope hypotheses.
why it matters
Direct input to the sibling non-vacuity theorem: in scope the $\mathbb{R}_{\ge 0}$ variance parameter of $\mu_N$ is nonzero, so the Gaussian is genuinely non-degenerate (not a Dirac mass). That sibling is labeled NON-VACUITY (target 4) of the preflight.
The result lives in QG full-theory campaign Phase 2b SLACK lane M, as candidate C10 preflight analysis. It is pure Mathlib-measure bookkeeping about gaussianReal on one Fourier mode. It does not touch the forcing chain T0–T8, the Recognition Composition Law, or any mass/alpha landmark; its only job is to keep the one-mode Gaussian non-degenerate under the fixed lattice normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.