← All papers
First page of Correlated and uncorrelated long–time asymptotics of type D ASEP

Correlated and uncorrelated long–time asymptotics of type D ASEP

Jeffrey Kuan

math-ph Jul 13, 2026 · v1 math.PR
Proofs of the type D ASEP long-time asymptotics were formalized in Lean using Aristotle by Harmonic AI.
The type D ASEP is an asymmetric two–species interacting particle system on $\Z$, in which two separately conserved species hop, bind into a composite “bound pair”, and split. The model, along with its reversible measures and orthogonal polynomial duality, was constructed using the representation theory of $U_q(\so_{2n})$. The reversible measures and orthogonal polynomial duality are each a product of two copies of the single-species ASEP reversible measures and orthogonal polynomial duality. In this paper, we study the long-time asymptotics of the type D ASEP. In the fixed–$q$ regime, using an exact current–decoupling identity, we prove that the asymptotic hydrodynamic limit and Tracy–Widom fluctuations decouple, as predicted from the duality. In the weak–asymmetry (Edwards–Wilkinson) regime, when $q=1-c/N^2$, we prove that the two density fluctuation fields decouple: each converges to a linear stochastic heat equation, with no cross–coupling in either the drift or the noise, the limiting noises having vanishing cross–correlation. More surprisingly, we then prove that the two limiting normal random variables are correlated with a seemingly new correlation function. The correlation is exactly equal to $(1-e^{-4c})/(4c)$, with the positive parts of the normal random variables having correlations expressed by the Bessel–Struve function. This paper, with the exception of the abstract and introduction, was written entirely by Claude Opus 4.8 and Fable 5. The proofs were then formalized in Lean, using Aristotle by Harmonic AI. The human author of this paper verified the proofs manually.

The type D ASEP is an asymmetric two-species interacting particle system whose long-time asymptotics were previously unknown. The question is how the two conserved species' density fluctuations behave and whether they decouple or correlate.

Using an exact current-decoupling identity, the asymptotic hydrodynamic limit and Tracy-Widom fluctuations are analyzed in the fixed-q regime. In the weak-asymmetry regime with q=1-c/N^2, the two density fluctuation fields are studied for cross-coupling in drift and noise. The proofs were generated by AI and formalized in Lean using Aristotle by Harmonic AI, with manual human verification.

The two density fluctuation fields decouple, each converging to a linear stochastic heat equation with no cross-coupling. The two limiting normal random variables are nonetheless correlated with correlation (1-e^{-4c})/(4c), and positive parts correlate via the Bessel-Struve function.