modeMeasure
plain-language theorem explainer
Defines the one-mode measure μ_N(k) as the centered real Gaussian on ℝ with variance v_N(k) = λ_N(k)^{-1}. Anyone citing the C10 cylinder preflight (characteristic functions, second moments, continuum limits) uses this object. It is a one-line packaging of Mathlib's gaussianReal at mean zero.
Claim. For $k,N\in\mathbb{N}$, the one-mode measure $\mu_N(k)$ is the centered Gaussian probability measure on $\mathbb{R}$ with 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 mode $k$ on the $N$-site unit circle.
background
This module is a one-mode toy preflight for the panel bet C10 (Gaussian cylinder-measure limit of a frozen quadratic energy). It treats a single Fourier mode $k$ on the $N$-site discretization of the unit circle (spacing $1/N$), and is explicitly not the path-sum measure and carries no campaign flag weight.
The lattice 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 quadratic $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k):=\lambda_N(k)^{-1}$. That variance is first formed as a real (modeVarianceReal), then packaged as a nonnegative real (modeVariance) because Mathlib's gaussianReal requires an $\mathbb{R}_{\ge 0}$ variance parameter.
The definition below is the actual Mathlib measure on $\mathbb{R}$ built from that variance, not a formal symbol.
proof idea
One-line definition: apply Mathlib's centered Gaussian constructor gaussianReal at mean $0$ with variance parameter modeVariance k N (the $\mathbb{R}_{\ge 0}$ packaging of $v_N(k)$). No tactics or lemmas beyond that constructor.
why it matters
This is the concrete measure object that every Target-1 and Target-3 identity in the preflight is stated about. Downstream it supplies: the probability-measure instance (non-vacuity); the moment-generating identity $\int e^{tx},d\mu_N=e^{v_N t^2/2}$; the characteristic function $\mathrm{charFun},\mu_N(t)=e^{-v_N t^2/2}$; the second-moment identity $\int x^2,d\mu_N=v_N$; and the continuum tendsto statements for both characteristic functions and second moments as $N\to\infty$ toward the continuum variance $(2\pi k)^{-2}$.
Within Recognition Science gravity analysis it is scaffolding for the C10 cylinder-measure story only: a genuine Mathlib Gaussian for one frozen mode, not a field-theoretic path measure and not linked to the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.