Sharp linear bounds for the EKG sequence

We prove that the EKG sequence satisfies $13n/28\le a(n)\le12n/7$ for every $n\ge1$, with equality only at $n=28$ and $n=7$, respectively. Discovered by Jonathan Ayres, the sequence starts with $1,2$ and repeatedly takes the least unused positive integer sharing a factor greater than $1$ with its predecessor. This proves the sharp linear bounds conjectured by Lagarias, Rains and Sloane, who established coarse bounds at every index. Hofman and Pilipczuk proved the limits $1/2$, $3/2$ and $1$ of $a(n)/n$ on primes, their triples and the other terms, and Haver made these estimates explicit and formalized them in Lean. Our earlier second-order asymptotic also builds on Haver's work. We sharpen Haver's self-improving early-even bound with a shorter prime window and effective large-sieve constants, and control odd terms so that the analytic range meets a finite computation. Lean checks the deduction from the definition, conditional on computed premises; independent programs check those premises, and their correspondence with the formal statements was checked by reading the code.

Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.