coe_modeVariance
plain-language theorem explainer
Coercing the nonnegative packaging of the one-mode Gaussian variance back to ℝ recovers exactly the real inverse lattice eigenvalue λ_N(k)⁻¹. Anyone wiring Mathlib's gaussianReal into continuum-limit arguments for a single Fourier mode needs this equality. The proof is a one-line application of Real.coe_toNNReal using nonnegativity of the real variance.
Claim. For every natural numbers $k$ and $N$, the coercion of the nonnegative real $v_N(k)$ (the mode variance packaged in $\mathbb{R}_{\ge 0}$) back to $\mathbb{R}$ equals the real-valued mode variance $v_N(k) = \lambda_N(k)^{-1}$, where $\lambda_N(k) = 4N^2\sin^2(\pi k/N)$ is the discrete Hessian eigenvalue of the frozen quadratic energy.
background
This module is a one-mode toy preflight for panel bet C10: a Gaussian cylinder-measure limit over a frozen quadratic energy on the $N$-site discretization of the unit circle. It is not the path-sum measure and carries no campaign flag weight. Everything is a genuine Mathlib statement about ProbabilityTheory.gaussianReal.
For Fourier mode $k \ge 1$, the lattice Hessian eigenvalue is $\lambda_N(k) := 4N^2\sin^2(\pi k/N)$. The Boltzmann weight of the frozen energy $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k) := \lambda_N(k)^{-1}$. That real number is modeVarianceReal; Mathlib's Gaussian constructor wants an $\mathbb{R}_{\ge 0}$ package, supplied by modeVariance := Real.toNNReal(modeVarianceReal).
The companion lemma modeVarianceReal_nonneg records $v_N(k) \ge 0$, which is the hypothesis needed to invert the toNNReal packaging without a residual max-with-zero.
proof idea
One-line term proof. Apply Real.coe_toNNReal to modeVarianceReal k N, discharging the nonnegativity side-condition by modeVarianceReal_nonneg k N. That lemma states that the inverse lattice eigenvalue is nonnegative, so coercion of toNNReal is the identity on the underlying real.
why it matters
The equality is the bridge between the $\mathbb{R}_{\ge 0}$ package required by Mathlib's Gaussian measure and the real-valued continuum-limit statements. Downstream, secondMoment_tendsto rewrites the second-moment integral via secondMoment_modeMeasure and this coercion, then invokes the real variance limit to get $\int x^2,d\mu_N \to (2\pi k)^{-2}$. The characteristic-function target charFun_modeMeasure_tendsto likewise depends on the packaged measure being faithful to $v_N(k)$.
In the Recognition gravity lane this is scaffolding for the one-mode cylinder preflight (Phase 2b SLACK lane M), not a forcing-chain step. It does not touch T0–T8, RCL, or the mass ladder; it only keeps the Mathlib measure API honest so later weak-convergence upgrades can cite a real Gaussian rather than a formal symbol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.