---

Claim. For all but $o(x)$ integers $n\le x$,

$$h(n)=\bigl(\tfrac12+o(1)\bigr)\log_* n,\qquad H(n)=(1+o(1))\log_* n,\qquad \frac{H(n)}{h(n)}=2+o(1).$$

This sharpens Treasure42's order-of-magnitude bounds to asymptotics with the constants $1/2$ and $1$: the ratio question is answered in the negative with the limit $2$, and Erdős's belief that $h(n)$ has normal order $\log_* n$ holds up to the constant $1/2$.

Argument. Both bounds descend the iterated tower $T_m=\exp T_{m-1}$. A chain step is bad when it is too short; for divisor chains a pair $d<e$ with $e\equiv1\pmod d$ and $e<\exp\sqrt d$ is bad, and the convergent tail $\sum_{d\ge Y}d^{-3/2}$ shows that almost no $n$ admits a large bad step, so each step climbs one tower level, giving $H(n)\le(1+o(1))\log_* n$. For prime chains the Brun--Titchmarsh inequality raises the bad threshold to $\exp\exp(p/(\log p)^2)$, which forces two tower levels per step and gives the constant $1/2$. The lower bounds are greedy constructions in the independent-prime model transferred by the Chinese remainder theorem: for $h$, a Siegel--Walfisz reciprocal-mass lemma finds a successor prime $q\equiv1\pmod{p_j}$ in each window; for $H$, a subset-product lemma for $K$ independent uniform elements of a finite abelian group of order $N$ (the probability that no nonempty subproduct is the identity is at most $N/(2^K-1)$) produces a squarefree composite successor $e\equiv1\pmod d$ from primes in Mertens-sized blocks whose residues modulo $d$ are nearly uniform by Siegel--Walfisz.

Claimant and systems. David Turturean posted the claim on 26 April 2026 and states that GPT-5.5 Pro produced the proof sketch and the patches to the write-up, assembled with Claude Code; the write-up is the Overleaf document linked above, with a revision of 1 May 2026 in Turturean's repository. Treasure42 posted on 27 April 2026 an alternative local successor argument, a Poisson-residue route to $H(n)\ge(1-o(1))\log_* x$, for checking; it proposes a different proof of part of this claim and is no separate result.

Formalizations. Three Lean developments formalize this result and are linked above at pinned revisions; none was built or audited by this corpus, so none is formalized evidence here.

• Turturean's repository (1 May 2026; main theorem erdos_696) has no sorry and admits three classical results as axioms, siegel_walfisz, brun_titchmarsh and mertens; its Lean was generated by Claude Opus 4.7 (Max Thinking) in Claude Code, as its README discloses.
• The erdos-lean repository's problems/696 folder, created on 31 May 2026 with Mertens' second theorem already proved, carried by 5 June 2026, when the thread announced it, Aristotle's proofs of Mertens' second theorem and the Brun--Titchmarsh inequality, leaving Siegel--Walfisz as the one axiom; at the pinned revision it holds the unconditional file below.
• Boris Alexeev's lean-proofs (26 August 2026) proves erdos_696 unconditionally, discharging Siegel--Walfisz from a Bombieri--Vinogradov development, and declares itself a formalization of the conditional argument linked from the thread.

Standing. The site's curator, Thomas Bloom, wrote on 11 May 2026 that Bloom had no reason to doubt these asymptotics but had not examined the longer proof carefully; the site's Lean qualification dates from that day and refers to Turturean's axiomatized development. One forum user reported a machine check of the write-up that found no issue and, after the Lean release, a machine check confirming the Lean file with its three axioms; another wrote that the axiomatized statements and the proof seemed correct, without reporting a check. None of this is independent review, refereed publication or a formalization built by this corpus, so the claim stays pending.