4 The initial-condition crossover (paper §7)
A martingale difference array with deterministic vanishing jump bound and bracket \(\to \sigma ^2\) has \(\mathbb E[e^{iuS_n}] \to e^{-u^2\sigma ^2/2}\), hence converges in law to \(N(0,\sigma ^2)\) (TypeDDecoupling.Levy.mcleish_clt_unconditional discharges the Lévy hypothesis).
Pointwise convergence of characteristic functions to that of a given probability measure implies weak convergence (identified-limit form), in one and two dimensions. (Mathlib master has since gained LevyConvergence.lean, post-dating this project’s pin — ours remains load-bearing at the pin.)
A locked-then-diagonal martingale array with random change point \(M_n/k_n \to U\) converges at the characteristic-function level to the \(U\)-mixture of correlation-\(u\) bivariate normals.
\((X_1,X_2)(T)/\sqrt{2T}\) converges to the mixture law with \(U \sim \min (\mathrm{Exp}(4c),1)\). Sorry-free via the documented process-level hypothesis bundle htwo.
The joint \(q\)-Laplace observable from the block equals the dual pair’s hitting probability on \(\mathbb Z\), with boundary constant \(k=0\). Sorry-free via the documented continuity hypothesis hcont; the finite-\(L\) core and the limit mechanism are proved.
The identity holds on every finite lattice, by matrix-exponential intertwining and exact block evaluation (modulo its named two-particle interlacing hypothesis).
\(\mathrm{Corr}(X_1,X_2) \to \rho (c) = (1-e^{-4c})/(4c)\), with monotonicity, the \(c\to 0\) and \(c\to \infty \) limits, and the \(1/(4c)\) tail.
\(\mathrm{Corr}(G_1^+,G_2^+) = \frac{\pi }{8(\pi -1)c}[1-2e^{-4c}+I_0(4c)-L_0(4c)]\), with besselI0/struveL0 as explicit power series.