modeVariance
plain-language theorem explainer
Packages the one-mode Gaussian variance v_N(k)=λ_N(k)^{-1} as a nonnegative real, the type Mathlib's centered Gaussian constructor demands. Anyone wiring the one-mode cylinder preflight measure, its characteristic function, or second-moment identities cites this cast. The body is a one-line Real.toNNReal of the real-valued inverse lattice eigenvalue.
Claim. For $k,N\in\mathbb{N}$, the mode variance is the nonnegative real $v_N(k):=\lambda_N(k)^{-1}$, obtained by casting the real inverse of the discrete Hessian eigenvalue $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ into $\mathbb{R}_{\geq 0}$.
background
This module is an honest one-mode toy preflight for panel bet C10: a Gaussian cylinder-measure limit over a frozen quadratic energy. It is not the path-sum measure and constructs no field-theoretic measure. Everything concerns a single Fourier mode $k$ on an $N$-site periodic lattice (unit-circle discretization, spacing $1/N$).
The discrete Hessian eigenvalue in lattice units is $\lambda_N(k):=4N^2\sin^2(\pi k/N)$, with continuum counterpart $(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}$. That real number is modeVarianceReal; Mathlib's gaussianReal needs the variance in $\mathbb{R}_{\geq 0}$, which is what this definition supplies.
Upstream, nonnegativity of $\lambda_N$ (hence of $v_N$) is immediate from the squared sine factor. Degenerate resolutions yield the junk value $0$ via Lean's $0^{-1}=0$.
proof idea
One-line definitional cast: apply Real.toNNReal to modeVarianceReal k N, i.e. to $(\lambda_N(k))^{-1}$. No tactics, no lemmas beyond the type coercion. Faithfulness of the cast (coe equals the real inverse) is proved separately once nonnegativity of the real variance is in hand.
why it matters
This is the variance parameter fed to the actual one-mode measure $\mu_N:=\mathrm{gaussianReal}(0,v_N(k))$, a genuine Mathlib probability measure on $\mathbb{R}$. Downstream it appears in the characteristic-function identity $\widehat{\mu_N}(t)=\exp(-v_N t^2/2)$, the moment-generating identity $\int e^{tx},d\mu_N=\exp(v_N t^2/2)$, the second-moment computation, the coe-faithfulness lemma, and the non-degeneracy statement that $v_N\neq 0$ under the in-scope bounds $1\le k$ and $4k\le N$.
In the QG campaign this sits in Phase 2b SLACK lane M as candidate C10 preflight scaffolding: it closes the type gap between the spectral eigenvalue and Mathlib's Gaussian API without introducing symbols, sorries, or axioms. It carries no flag weight and is deliberately separate from the Test G lane. Framework-wise it is local analysis on the frozen quadratic, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.