modeVarianceReal_nonneg
plain-language theorem explainer
The one-mode Gaussian variance v_N(k) = λ_N(k)^{-1} is nonnegative for every Fourier mode k and lattice size N. Anyone packaging the centered Gaussian cylinder measure on a single mode needs this before coercing into ℝ≥0. The proof is a one-line application of nonnegativity of the reciprocal to the already-proved nonnegativity of the discrete Hessian eigenvalue.
Claim. For all natural numbers $k$ and $N$, the one-mode variance $v_N(k) := \lambda_N(k)^{-1}$ satisfies $v_N(k) \ge 0$, 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 circle.
background
This module is a one-mode toy preflight for 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$), and is explicitly not the path-sum measure and carries no campaign flag weight.
The discrete Hessian eigenvalue is $\lambda_N(k) := 4N^2\sin^2(\pi k/N)$ (latticeEigenvalue). Its continuum counterpart is $(2\pi k)^2$. The Boltzmann weight of the frozen quadratic $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k) := \lambda_N(k)^{-1}$ (modeVarianceReal), with Lean's convention $0^{-1}=0$ at degenerate resolutions. The nonnegative packaging modeVariance feeds Mathlib's gaussianReal.
Upstream, latticeEigenvalue_nonneg already records $\lambda_N(k)\ge 0$ (it is $4N^2$ times a square).
proof idea
One-line term proof. Apply Mathlib's inv_nonneg.mpr to the hypothesis latticeEigenvalue_nonneg k N, which states $0\le\lambda_N(k)$. Nonnegativity of the reciprocal immediately yields $0\le\lambda_N(k)^{-1}$, i.e. $0\le v_N(k)$.
why it matters
Feeds coe_modeVariance, which asserts that the $\mathbb{R}_{\ge 0}$ packaging is faithful: coercing modeVariance k N back to $\mathbb{R}$ recovers exactly $\lambda_N(k)^{-1}$. That faithfulness is required before the one-mode measure can be identified with Mathlib's centered gaussianReal of variance $v_N(k)$, and before non-vacuity (probability-measure instance) and moment identities (characteristic function, second moment) can be stated without junk coercions.
In the broader Recognition gravity lane this is Phase 2b SLACK preflight for panel bet C10: a Gaussian cylinder-measure limit over the frozen quadratic energy. It sits downstream of the spectral-convergence control $|\lambda_N(k)-(2\pi k)^2|\le((2\pi k)^4/12)/N^2$ and upstream of genuine Mathlib measure statements. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is pure analytic hygiene for the one-mode toy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.