modeVarianceReal
plain-language theorem explainer
One-mode Gaussian variance on the N-site lattice equals the reciprocal of the discrete Hessian eigenvalue λ_N(k)=4N²sin²(πk/N). Cylinder-measure and spectral-convergence work cite it as the Boltzmann variance of the frozen quadratic energy for Fourier mode k. Definitional one-liner; Lean's 0⁻¹=0 supplies a junk value at degenerate resolutions.
Claim. For $k,N\in\mathbb{N}$, the one-mode lattice variance is $v_N(k):=\lambda_N(k)^{-1}$, where $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ is the discrete Hessian eigenvalue of Fourier mode $k$ on the $N$-site periodic unit-circle lattice. When $\lambda_N(k)=0$, the reciprocal is taken to be $0$ by convention.
background
This module is a one-mode toy preflight for panel bet C10 (Gaussian cylinder-measure limit over the frozen quadratic energy). It is not the path-sum measure and carries no campaign flag weight: everything concerns a single Fourier mode $k$ on a one-dimensional $N$-site periodic lattice of spacing $1/N$.
The discrete Hessian eigenvalue in lattice units is $\lambda_N(k):=4N^2\sin^2(\pi k/N)$, the exact expression whose quantitative continuum expansion $|\lambda_N(k)-(2\pi k)^2|\le((2\pi k)^4/12)/N^2$ is proved in SpectralConvergence. The continuum eigenvalue 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 the frozen quadratic energy $\tfrac12\lambda x^2$ is the centered real Gaussian of variance $v_N(k):=\lambda_N(k)^{-1}$. That real is later packaged as a nonnegative real for Mathlib's gaussianReal.
proof idea
Definitional one-liner: the real variance is the multiplicative inverse of the lattice eigenvalue. No tactics or lemmas fire. Lean's field inverse sends zero to zero, which the doc-comment records as the intentional junk value when the mode is degenerate.
why it matters
Local parent of the nonnegative packaging used by the actual one-mode measure, of the coercion faithfulness lemma, of nonnegativity and in-scope strict positivity, of the $O(1/N^2)$ rate $|v_N(k)-(2\pi k)^{-2}|\le(1/6)/N^2$, and of pointwise characteristic-function convergence to the continuum Gaussian. Those are Targets 2--3 of the C10 preflight (rate and charFun tendsto); the module honesty header stresses this is separate from Test G and flips no flag. It is the lattice-side variance input that makes the frozen-quadratic Boltzmann weight a genuine Mathlib Gaussian rather than a formal symbol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.