7 Layer L4: probability primitives
White noise via random Fourier series, the Isserlis/Wick theorem, and the minimal chaos API. No parametrix objects appear here.
The canonical probability space of independent standard real Gaussians, two per \(\{ \pm k\} \)-orbit and one for the zero mode; the assembled complex coefficients \(g_k\) with \(\mathbb {E}[g_k g_l] = \mathbf{1}_{k=-l}\), \(\mathbb {E}[g_k \overline{g_l}] = \mathbf{1}_{k=l}\); the mollified noise \(\xi _\varepsilon = (2\pi )^{-2}\sum _k \widehat\rho (\varepsilon k)\, g_k e_k\) (the Lebesgue/probability-Haar half-density from the normalization ledger), a.s. \(C^\infty \), with a single probability-one event working simultaneously for every countable scale family; the covariance identity \(\mathbb {E}[\xi _\varepsilon (x)\xi _\varepsilon (y)] = \eta _\varepsilon (x-y)\), \(\eta = \rho * \rho \).
For a finite jointly-Gaussian centered family, \(\mathbb {E}\big[\prod _j X_j\big] = \sum _{\kappa \text{ full pairing}} \prod _{\{ i,j\} \in \kappa }\mathbb {E}[X_iX_j]\), proved by a self-contained induction.
Induction on the family size for the canonical coordinate Gaussians, then transport to the assembled complex coefficients \(g_k\) via the orbit generators.
Moments of \(\prod _j \xi _\varepsilon (x_j)\) as sums over full pairings of \(\eta _\varepsilon \)-factors; the chaos decomposition of products with partial pairings and \(\mathrm{Proj}_{\lvert S\rvert }\).
Isserlis applied to the mode coefficients, resummed against the covariance identity \(\mathbb {E}[\xi _\varepsilon \xi _\varepsilon ] = \eta _\varepsilon \); the explicit Wick sum agrees with the chaos-projection product by the pair-product/Wick-polynomial decomposition.
Convergence of all joint moments to those of a Gaussian vector implies convergence in distribution (moment determinacy of Gaussians; finite-dimensional). Realized in the fixed-truncation form consumed by the assembly.
Real joint moments of the fixed truncation converge to the Gaussian moments; dominated exponential-series comparison upgrades this to characteristic functions.
Filter-indexed convergence-in-distribution lemmas for realified mode vectors (mathlib’s sequence-indexed statements transported to the \(\varepsilon \)-filter); restriction to good events of probability tending to one.
Characteristic-function convergence along the \(\varepsilon \)-filter yields convergence of the pushforward probability measures; the law-level main statement follows from the characteristic-function form.