Correlated and uncorrelated long-time asymptotics of type D ASEP: formalization blueprint

5 The Tracy–Widom regime (paper §8)

Theorem 5.1 TW marginals; Thm. 8.1
#

For every \(n\) and each species the standardized current converges to \(F_2\). Sorry-free; reduces to the cited single-species step-ASEP input (carried as a hypothesis) via 1.3.

Theorem 5.2 \(q\)-Laplace decoupling; Thm. 8.3

The exact contact representation: \(\mathbb E[q^{2N_i}]\) and \(\mathrm{Cov}(q^{2N_1},q^{2N_2})\) as absolutely convergent dual sums, the covariance generated entirely by contact.

Definition 5.3 the covariance conjecture; Conj. 8.5
#

The statement \(\mathrm{Cov}(N_1,N_2)(s) \sim c(q)\sqrt s\) with \(c(1/2) = 0.099 \pm 0.003\) (Monte Carlo), as a named Prop-valued definition — no truth claim is made; anyone wishing to use it must supply a proof of covConjecture explicitly.