The second-order asymptotic of the EKG sequence

The EKG sequence $a(n)$ starts $1,2$ and thereafter chooses the least unused positive integer not coprime to the preceding term. Jonathan Ayres discovered it, and Lagarias, Rains and Sloane conjectured its additive second-order asymptotic at almost all indices. Haver reduced the asymptotic for the least unused even integer to counting used odd values above it, excluding three times odd primes, and proved the sharp upper bound. Hofman and Pilipczuk proved the weaker ratio limits and prime pattern. Combining these estimates with an elementary sieve and the prime number theorem, we prove the lower bound and transfer to the smoothed sequence. Smoothing $p,3p$ to $2p$ for odd primes gives $b(n)=n+n/(3\log n)+o(n/\log n)$ $(n\to\infty)$, hence the conjectured formula at almost all original indices. We prove Ordowski's nonprime inequality and density-one conjectures, and Jasinski's finiteness conjectures for the three critical lines; we also obtain the below-diagonal asymptotic and finiteness of cycles of each bounded length. Lean formalizes the main theorem.

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