charFun_modeMeasure_tendsto
plain-language theorem explainer
Pointwise, the characteristic function of the single-mode lattice Gaussian converges to that of the continuum centered Gaussian of variance $(2\pi k)^{-2}$. Anyone auditing the C10 cylinder-measure preflight cites this as Target 3. The proof is continuity of complex exponential on the already-proved variance limit, matched to the closed form of the mode characteristic function. No Lévy upgrade is claimed.
Claim. For every Fourier mode $k \ge 1$ and every real $t$, as $N \to \infty$ the characteristic function of the centered Gaussian of variance $\lambda_N(k)^{-1}$ (inverse discrete Hessian eigenvalue on the $N$-site unit circle) tends to $\exp\bigl(-(2\pi k)^{-2}\, t^2/2\bigr)$, the characteristic function of the continuum centered Gaussian of variance $(2\pi k)^{-2}$.
background
This module is a one-mode toy preflight for campaign bet C10: a Gaussian cylinder-measure limit for the 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 discretization of the unit circle (spacing $1/N$).
The discrete Hessian eigenvalue is $\lambda_N(k) := 4N^2\sin^2(\pi k/N)$ (latticeEigenvalue). Its continuum counterpart is $(2\pi k)^2$ (continuumEigenvalue), the $-d^2/dx^2$ eigenvalue of $e^{2\pi i kx}$ on the unit circle. The Boltzmann weight of $\tfrac12\lambda x^2$ is the centered real Gaussian of variance $v_N(k):=\lambda_N(k)^{-1}$ (modeVarianceReal), packaged as the probability measure modeMeasure.
Upstream, modeVarianceReal_tendsto already gives $v_N(k)\to(2\pi k)^{-2}$ for $k\ge 1$, using the quantitative sine-eigenvalue expansion from SpectralConvergence. The mode characteristic function is known in closed form: $\varphi_{\mu_N}(t)=\exp(-v_N(k),t^2/2)$.
proof idea
Term-mode continuity chase. First lift the real variance limit through Complex.continuous_ofReal to get complex-valued convergence of $v_N(k)$ to $(2\pi k)^{-2}$. Multiply by the constant $t^2$, divide by $2$, and negate, preserving the limit. Apply continuity of complex exponential to obtain convergence of $\exp(-v_N t^2/2)$ to the target Gaussian characteristic function. Finally rewrite the left-hand side via charFun_modeMeasure and coe_modeVariance, which identify the mode characteristic function with that exponential of the real variance.
why it matters
Target 3 of the one-mode cylinder preflight: the strongest pointwise convergence statement available in the vendored Mathlib without new axioms. Because Lévy's continuity theorem is not in scope, the classical upgrade from pointwise characteristic-function convergence to weak convergence of measures is deliberately not claimed; this lemma stops at the characteristic-function limit.
In the Recognition gravity lane this is scaffolding toward a Gaussian cylinder measure over the frozen quadratic energy (panel bet C10), not a campaign flag flip. It sits downstream of the spectral continuum limit $\lambda_N(k)\to(2\pi k)^2$ and of the exact Gaussian characteristic-function formula for each finite $N$. No used_by edges are recorded yet; the immediate next target in-file is non-vacuity of the limiting variance (strict positivity of $(2\pi k)^{-2}$ for $k\ge 1$), ensuring the limit object is a non-degenerate Gaussian rather than a point mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.