instIsProbabilityMeasureModeMeasure
plain-language theorem explainer
For every Fourier mode index k and lattice size N, the one-mode centered Gaussian μ_N is a probability measure on ℝ. Anyone working the C10 cylinder-measure preflight cites this as the non-vacuity gate before moment or characteristic-function identities. The proof unfolds the definition and inherits Mathlib's gaussianReal probability-measure instance.
Claim. For all $k,N\in\mathbb{N}$, the centered real Gaussian measure $\mu_N$ of variance $v_N(k)=\lambda_N(k)^{-1}$ (with lattice Hessian eigenvalue $\lambda_N(k)=4N^2\sin^2(\pi k/N)$) is a probability measure on $\mathbb{R}$.
background
This module is a one-mode toy preflight for the panel bet C10 (Gaussian cylinder-measure limit of a frozen quadratic energy). It is not the path-sum measure: everything concerns a single Fourier mode $k$ on the $N$-site periodic lattice of the unit circle.
The discrete Hessian eigenvalue is $\lambda_N(k):=4N^2\sin^2(\pi k/N)$, with continuum counterpart $(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}$, packaged as the Mathlib measure gaussianReal of mean $0$ and that variance. The object here is exactly that measure $\mu_N$.
The module header stresses fixed a-priori normalization, genuine Mathlib measure statements, and no campaign-flag weight. Non-vacuity (target 4) is the prerequisite for the moment-generating and characteristic-function identities proved next in the same file.
proof idea
One-line wrapper. Unfold the definition of the mode measure (the centered gaussianReal of variance $v_N(k)$), then infer_instance discharges IsProbabilityMeasure from Mathlib's existing Gaussian probability-measure instance. No custom measure construction or positivity argument is written by hand.
why it matters
Closes non-vacuity target 4 in the C10 one-mode cylinder preflight: before any integral identity against $\mu_N$ is meaningful, $\mu_N$ must be a probability measure for every mode and lattice size. Sibling targets in the same module (moment-generating identity $\int e^{tx},d\mu_N=e^{v_N t^2/2}$, characteristic function, second moment) sit on top of this instance.
In the broader Recognition gravity lane this is scaffolding hygiene only. The module carries no flag weight, does not touch the path-sum measure, and is deliberately separate from Test G. Framework landmarks (T0–T8, RCL, eight-tick) are upstream context for why a quadratic frozen energy appears; they are not invoked in the proof. No open campaign question is discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.