secondMoment_modeMeasure
plain-language theorem explainer
The second moment of the one-mode centered Gaussian equals its variance parameter v_N(k). Anyone working the C10 cylinder-measure preflight (single Fourier mode on the N-site circle) cites this identity before taking N→∞ limits. The argument is a short Mathlib reduction: variance of a zero-mean real Gaussian is the integral of x².
Claim. For $k,N\in\mathbb{N}$, if $\mu_{k,N}$ is the centered real Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$ (with $\lambda_N(k)=4N^2\sin^2(\pi k/N)$ the discrete Hessian eigenvalue), then $\int x^2\,d\mu_{k,N}=v_N(k)$ as a real number.
background
This module is an honest one-mode toy preflight for panel bet C10: a Gaussian cylinder-measure limit over the frozen quadratic energy on the unit circle. It is not the path-sum measure, carries no campaign flag weight, and treats a single Fourier mode $k$ on an $N$-site periodic lattice (spacing $1/N$).
The discrete Hessian eigenvalue is $\lambda_N(k)=4N^2\sin^2(\pi k/N)$. The continuum counterpart is $(2\pi k)^2$. The Boltzmann weight of the frozen energy $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$, packaged as a nonnegative real and as the probability measure $\mu_{k,N}$.
Mathlib supplies the real Gaussian API (gaussianReal) and the identity that variance of the identity map equals $\int(x-\mu)^2$. Here the mean is zero, so that collapses to $\int x^2$.
proof idea
Invoke Mathlib's variance_fun_id_gaussianReal at mean $0$ and variance $v_N(k)$. Rewrite variance as an integral via variance_eq_integral (identity is a.e. measurable). Simplify with the zero-mean Gaussian integral identity and sub_zero, which yields $\int x^2=v_N(k)$. Unfold the definition of the mode measure and finish by exact match. Pure term-mode reduction; no new analysis.
why it matters
This is Target 1 of the one-mode preflight: the second-moment functional on $\mu_{k,N}$ is exactly the variance parameter, so continuum limits of second moments reduce to limits of $v_N(k)$ alone.
Downstream, secondMoment_tendsto applies it: after rewriting the integral by this identity and coercing the nonnegative variance, the $N\to\infty$ limit of $\int x^2,d\mu_{k,N}$ is the continuum mode variance $(2\pi k)^{-2}$, using the already-proved variance tendsto. That is Target 3 of the same file.
In the broader RS gravity lane this is scaffolding for a Gaussian cylinder-measure story over frozen quadratic energy, not yet the full path-sum or QG measure. It sits in Phase 2b SLACK lane M and stays deliberately separate from Test G.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.