charFun_modeMeasure
plain-language theorem explainer
For each Fourier mode k on the N-site circle, the characteristic function of the centered Gaussian one-mode measure equals exp(−v_N t²/2), with v_N the inverse lattice Hessian eigenvalue. Anyone tracking the C10 cylinder-measure preflight cites this as the exact finite-N formula. The proof unfolds the measure definition and applies Mathlib's gaussian characteristic-function identity, then simplifies the complex cast by ring.
Claim. For natural numbers $k,N$ and real $t$, if $\mu_N$ is the centered real Gaussian measure of variance $v_N(k)=\lambda_N(k)^{-1}$ (with $\lambda_N(k)=4N^2\sin^2(\pi k/N)$), then its characteristic function satisfies $\varphi_{\mu_N}(t)=\exp(-v_N(k)\,t^2/2)$.
background
This module is a 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 the $N$-site periodic lattice (unit-circle discretization, spacing $1/N$).
The discrete Hessian eigenvalue is $\lambda_N(k):=4N^2\sin^2(\pi k/N)$. The Boltzmann weight of the frozen quadratic $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k):=\lambda_N(k)^{-1}$, packaged as a nonnegative real and fed to Mathlib's gaussianReal. The one-mode measure is exactly that centered Gaussian on $\mathbb{R}$.
Characteristic functions are the standard Fourier transforms of probability measures. For a centered real Gaussian of variance $v$, Mathlib already records $\varphi(t)=\exp(-v t^2/2)$. This declaration simply specializes that identity to the mode measure.
proof idea
Term-mode, four steps. Unfold the definition of the one-mode measure to expose gaussianReal 0 (modeVariance k N). Rewrite by Mathlib's charFun_gaussianReal, which gives the centered-Gaussian formula with mean zero. Congruence on the exponential argument, then push_cast and ring align the nested real-to-complex coercions of the variance and of $t^2/2$. No mode-specific analysis is required beyond the definition.
why it matters
This is TARGET 1 of the one-mode cylinder preflight: the exact finite-$N$ characteristic function. Downstream, charFun_modeMeasure_tendsto (TARGET 3) uses it to pass to the continuum limit pointwise in $t$, obtaining $\varphi_{\mu_N}(t)\to\exp(-(2\pi k)^{-2}t^2/2)$, the characteristic function of the continuum Gaussian of variance $(2\pi k)^{-2}$. That is the strongest convergence statement available without a Lévy continuity theorem in the vendored Mathlib, so weak convergence is deliberately not claimed.
In the broader QG campaign this sits in Phase 2b SLACK lane M as honest scaffolding toward C10, carrying no campaign flag. It anchors the finite-$N$ side of the spectral bridge already proved for $\lambda_N(k)\to(2\pi k)^2$ in SpectralConvergence. Within Recognition Science gravity analysis it is pure measure theory on the frozen quadratic mode, not a claim about eight-tick structure, $D=3$, or the full path measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.