← All papers
First page of Exact determinant formulas for coalescing particle systems

Exact determinant formulas for coalescing particle systems

Piotr Śniady, Ákos Urbán

math.PR Feb 11, 2026 · v3 math.CO
The paper's discrete results, the coalescence determinant formulas for spacetime graphs, are formalized and machine-checked in Lean 4 in a deposited artifact.
When particles on a line collide, they may coalesce into one. Such systems arise in the voter model, where boundaries between opinion clusters perform coalescing random walks, and in reaction-diffusion theory, where diffusing particles merge on contact. Computing exact coalescence probabilities has been difficult because collisions reduce the particle count, while classical determinantal methods require a fixed number of particles throughout. We introduce ghost particles: when two particles collide, one survivor continues as usual and one invisible ghost is created alongside it, preserving the total count. This restores the square matrix structure needed for a determinantal formula. We prove that the probability of any specified coalescence pattern - which initial particles merge into which survivors - is given by a determinant whose entries are transition probabilities. Integrating out ghost positions yields a closed-form formula for the surviving particles alone: the coalescence determinant. The only assumptions are the Markov property and nearest-neighbor transitions, so the results apply wherever the classical non-colliding theory does: discrete lattice paths, birth-death chains, and continuous diffusions including Brownian motion.

Classical determinantal formulas such as Karlin–McGregor and Lindström–Gessel–Viennot require a fixed number of non-colliding particles. They fail for coalescing particle systems, such as those in the voter model, where collisions reduce the particle count.

When two particles collide, the method creates an invisible ghost particle alongside the survivor, which preserves the particle count and restores a square matrix. The proof works on abstract spacetime graphs with planarity and weight-preserving segment swaps. It uses a Leibniz expansion with ghost-adjusted signs, an attribution/rehearsal bijection between performances and successful castings, and a sign-reversing involution at the first spurious crossing. The discrete results are formalized in Lean 4, together with a Python reference implementation.

The probability of any specified coalescence pattern equals a determinant of transition probabilities. Integrating out ghost positions gives a closed-form coalescence determinant for the survivors. The results apply to lattice walks, birth-death chains, and continuous diffusions including Brownian motion.