Divergence of $\sum 1/a_i$ for the Eggleton–Erdős–Selfridge coprime sequence (Erdős #460)

Fix a positive integer $n$. Define a sequence by $a_0=0$, $a_1=1$, and for $k\geq 2$ let $a_k$ be the least integer $>a_{k-1}$ such that $\gcd(n-a_k,\,n-a_i)=1$ for all $0\leq i<k$. Does $$\sum_{0<a_i<n}\frac{1}{a_i}\to\infty\quad\text{as }n\to\infty\,?$$ The same question is asked for the sum restricted to those $i$ for which $n-a_i$ is divisible by some prime $\leq a_i$, and for the sum over the complementary set of $i$. (The restriction $a_i<n$ in the sum is essential: without it the sum is infinite, since the sequence contains $n+p$ for every prime $p>n$.)

Acceptance. FULLY RESOLVES (proof-shaped): a complete proof — machine-checkable (Lean/Coq) preferred, else fully written — settling whether $\sum_{0<a_i<n}1/a_i\to\infty$ for the main formulation above (and, for full credit, the two restricted variants). ADVANCES: a proof that Chojecki's sufficient condition $f(n)\to\infty$ holds; a proof of the conjectured growth $a_k\ll k\log k$, strictly improving the recorded $a_k<k^{2+o(1)}$ bound; or a reproducible computation of $a_k$ and of the partial sums $\sum_{0<a_i<n}1/a_i$ over a substantially extended range of $n$ and $k$, with the program and certified data, that supports or rules out divergence. Deliver the proof, or the computation code plus tabulated growth data.