Papers With

← All papers
First page of Uniform Bessel bounds for endpoint crossings in the persistent random walk

Uniform Bessel bounds for endpoint crossings in the persistent random walk

Arjun Pemmasani

math.PR Oct 3, 2026 · v1 cond-mat.stat-mech
formalization probability combinatorics
Read PDF arXiv abstract Code
TL;DR
Many results, including the explicit crossing bracket for all N≥2, are formalized in Lean 4. The Lean kernel rechecks the integer certificates for N≤174.
Abstract
A ball bounces down a Galton board, where its first bounce's direction is fair while every later bounce repeats the previous bounce's direction with probability $p$, all the way down to some bin. We ask for which $p$ the middle bin is exactly as likely as the end bins, a question originally posed by Kagey. We find that for $N$ bounces, the tie occurs when the ball changes direction (turns) approximately $\log N$ times on average. We compare the central bin with a Bessel function, with an error bound that is explicit for all $N$. This yields an explicit interval for the tie at every $N \geq 2$, rather than just for large $N$. This is done analytically for $N \geq 175$, and for smaller $N$ exactly by integer arithmetic, cross-verified in Lean. We also find the tie of every other bin with the end bins and the shift caused by periodic boundaries.
Problem

Kagey's Problem 131 asks for which persistence parameter p the middle bin of a Galton board with momentum (a persistent random walk) is exactly as likely as the end bins. The paper seeks explicit bounds on this crossing for every N, not only asymptotically.

Approach

The bin law is written as a sum over the number of direction switches. The middle-to-endpoint ratio is compared with Bessel functions I_0 and I_1, using error bounds that are explicit for all N. For N≥175 the crossing interval is derived analytically. For 2≤N≤174 it is decided by exact integer-arithmetic certificates at rationals on either side of the root, which the Lean 4 kernel rechecks. The formalization was generated with AI assistance and reviewed by hand.

Results

N(1-p_N) = log N − ½ log log N − 0.467… + o(1). An explicit bracket for the crossing holds at every N≥2 and is formalized in Lean using only standard axioms. The paper also gives the crossings for every other bin, and shows that periodic boundaries shift the central crossing by about (log 2)/N in the odds.