3 The Edwards–Wilkinson regime (paper §6)
For all densities \(\rho _1,\rho _2 \in (0,1)\), \(\langle W_{i,x}, B_z\rangle = 0\) for every \(z\), where \(B_z = (\eta _{1,z}-\rho _1)(\eta _{2,z}-\rho _2)\). Proved from the equilibrium product (independence) structure of the blocking measure (the EWModel structure): the species-\(i\) current depends only on species-\(i\) occupations, so it factorizes against the opposite-species centred field, whose mean vanishes.
\(\langle V_x, \eta _{i,y}-\rho _i\rangle = 0\) for every species \(i\) and sites \(x,y\): \(V_x\) has no order-one component, its lowest order being two. Proved by the general involution argument EqvarOrth.expect_V_mul_occ_eq_zero (swapping the other species across the bond reverses the sign of \(V_x\) while fixing the blocking weight), realised concretely as the covariance ewCrossDensityCov over a finite blocking-measure window.
With \(\Theta ^N = N^{-1}\sum _x \varphi '(x/N)^2 V_x\): \(\mathbb E_\nu [(\Theta ^N)^2] \le C(\varphi )N^{-1}\), via the exact cancellation \(\mathbb E[V_xV_y]=0\) for \(|x-y|\ge 2\) and \(|V|\le 1\) (EqvarOrth.expect_sq_le). The boundedness hypothesis on \(\varphi '\) is genuinely needed (the bare statement over arbitrary coefficients is false).
With \(\beta _i = \alpha _i/(1+\alpha _i)\): the blocking measure and the reweighted measure have the same sector conditionals, uniformly comparable sector masses (\(\log M \le 2C_0\), \(C_0 = A(1+\tfrac {8\beta }{1-\beta })\), \(A = 18cK^2\) under the regime-A scaling), and the correlation transfer inequality holds. Replaces a FALSE original (the uncompensated comparison has \(M = e^{\Theta (N)}\)); cores TypeDDecoupling.Sector.sector_comparison_single, TypeDDecoupling.Sector.correlation_transfer.
\(\| V_z^{(\mathrm{dr})}\| ^2_{L^2(\varpi )} \le \varepsilon _N = (q_N^{-4|\Lambda |}-1)^2 = O(N^{-2}) \to 0\), uniformly over \(z\) in the field window, via the exact identity \(A_z = q^{-2(L_1+L_2)}V_z\) and the projection inequality (core TypeDDecoupling.DressedMass.dressedMass_bond_le); the dressed mass is realised concretely on the regime-A window with \(q_N = 1-1/(N+2)^2\).
\(\mathbb E_\nu [\langle M_1^N,M_2^N\rangle (\varphi ,t)^2] \le C(\varphi ,c)\, t\, (N^{-1} + N^{-2}\log _+(tN^2) + t\, \varepsilon _N) \to 0\) (condition (X)). Sorry-free from the abstract estimate TypeDDecoupling.Conc.conc_master; the process-level inputs (transfer bound, mass-sector kernel split, equal-time bound, stationarity identity) enter as the named hypothesis hproc. The truncated \(\log _+\) is a fidelity repair: the bare \(\log \) would be false for small \(t\).
\(\Gamma _i^N(\varphi ,\cdot ) \to D\, Y_i(\Delta \varphi ,\cdot )\) in \(L^2\) (condition (D)). Quantitative cores proved outright: summation-by-parts + Taylor (TypeDDecoupling.Drift.drift_sbp_bound) and the correction second moment (TypeDDecoupling.Drift.corr_second_moment); the \(\mathcal S'(\mathbb R)\) wrapper enters as the hypothesis hpin.
\(M^f_t = f(\eta _t)-f(\eta _0)-\int _0^t Lf(\eta _s)ds\) is a martingale against Mathlib’s \(\mathbb R\)-indexed Martingale (core TypeDDecoupling.dynkin_martingale, from a faithful Markov–Feller bundle), the bracket is definitionally the carré-du-champ time integral (dynkinBracketDef; the identification with the predictable bracket is the cited Ethier–Kurtz Ch. 4 fact), and the integrated covariance identity \(\mathbb E[M^f_tM^g_t] = \mathbb E\int _0^t \Gamma (f,g)(\eta _s)ds\) is proved (core TypeDDecoupling.dynkin_L2). The former opaque predicates are retired.
If, for every \(\varphi \in \mathcal S(\mathbb R)\), the path processes \(t\mapsto \langle Z_N(t),\varphi \rangle \) have tight laws on \(D([0,1];\mathbb R)\), then for every \(\eta {\gt}0\) the processes are confined, uniformly in \(N\) and with probability \(\ge 1-\eta \), in a single compact polar ball of the pointwise dual \(\mathcal S'(\mathbb R)\) (Kallianpur–Xiong compact-confinement form of Mitoma’s theorem; the classical iff against a topology on \(D([0,1];\mathcal S')\) is deliberately not formalized). Proved from the Hermite–Sobolev nuclear chain and the uniform confinement theorem; formerly the project’s one remaining citation sorry, now discharged (fidelity-repair note in the Lean docstring).
Restated as a genuine theorem over probability spaces (no longer a citation): a family \((X_i)\) of \(D([0,1];\mathbb R)\)-valued random elements on probability spaces \((\Omega _i, P_i)\), each adapted to a right-continuous filtration, whose laws are (i) uniformly bounded in sup-norm in probability and (ii) satisfy the Aldous stopping-time condition (\(\alpha _i(\delta ,\varepsilon ) \to 0\) uniformly in \(i\)), has tight pushforward laws on the Skorokhod space (IsTightMeasureSet). Proved by direct application of SkorokhodBasic.aldous_tightness (6.15).
From the de-opaqued bracket condition mpConvBracket — per test function \(\varphi \) and time \(t\), a martingale-difference array with deterministic bracket \(2\chi Dt\, \sigma (\varphi )\) and a stopped/truncated companion — the pairing characteristic function of \(Z_t^N\) converges to the centered Gaussian \(\exp (-(2\chi Dt\, \sigma (\varphi ))u^2/2)\); via the stopped-array adapter and the project’s own martingale CLT.
A process whose Dynkin drift converges to \(DZ(\Delta \varphi )\) (mpConvDrift), whose bracket converges to \(2\chi Dt\| \partial \varphi \| ^2\) (mpConvBracket), and which is Mitoma-tight, converges in law to the stationary OU solution. The Gaussian/uniqueness core is proved from 3.11; only the path-space existence/convergence content enters as the single documented bundle MPPathBundle (riding on the Mitoma/Aldous leaves and the heat-semigroup identification). Sorry-free.
Each single-species fluctuation field converges to the Gaussian OU/EW field with diagonal bracket \(2\chi Dt\| \partial \varphi \| ^2\), \(\chi = \rho (1-\rho )\). Proved outright as the single-field case of 3.12 (same faithful hypotheses); the Dittrich–Gärtner reference is demoted to a classical-instantiation citation.
The finite-\(N\) ground truth making the bracket hypothesis of 3.13 faithful for the stationary single-species WASEP under the Bernoulli(\(\rho \)) product weight: exact equilibrium mean \(2\chi D\| \varphi '\| ^2\) with \(D = (1+q^2)/2\), variance \(O(1/N)\), and \(L^2\) concentration of the time-integrated bracket under stationarity.
Under \(q = 1-c/N^2\) the rescaled density-fluctuation pair is tight in \(D([0,T];\mathcal S'(\mathbb R))\) and converges to two independent stationary Edwards–Wilkinson (OU) fields, at arbitrary densities; the limiting cross bracket vanishes (condition (X)) and the corrected sector comparison holds. Rewired to two real-tightness hypotheses \(ht_1, ht_2\) (component tightness of the evaluated processes — exactly what 3.10 produces), fed through 3.9 for the \(\mathcal S'\)-tightness; the OU limits come from 3.12 and 3.13, the decoupling from 3.5, 3.6 and 3.4. The declaration itself is sorry-free; it inherits the project’s single remaining citation sorry transitively through its use of 3.9.