Kernel-Checked Frontier Certificates for Erdős Problem 414

Abstract

Let $h(n)=n+\tau (n)$, where $\tau$ counts divisors. Erdős and Graham asked, after Spiro, whether the orbits of any two positive integers under $h$ eventually share a point (Problem 414 on Bloom's list). The problem is open, and a finite computation cannot close it; nothing about it has been checked by a proof kernel, and the statement in the formal-conjectures repository carries a sorry. We replay what can be certified through the Lean 4 kernel under an axiom gate (axioms exactly propext, Classical.choice, Quot.sound; no sorry; no native_decide). Three elementary facts recorded by Li, namely that coalescence is an equivalence relation, $\tau (n)$ is odd exactly for squares, and $\tau (n)$ is bounded by $2\sqrt{n}$ so that orbits skip no square annulus $[k^2,(k+1{)}^2)$, are formalized, and his frontier lemma is formalized in a window form: every orbit started below a level $N$ has a point within $\lceil 2\sqrt{N}\rceil$ below $N$. The frontier lemma becomes a certificate: the $\lceil 2\sqrt{N}\rceil$ values $\tau (m)$ just below $N$ and the orbit points above $N$ until the orbits through the crossing points have merged. Its soundness is a kernel-checked theorem, and the certified rungs state that every pair of positive integers below $N$ coalesces for $N=10^5,10^6,10^7,10^8$; the certificate at $10^8$ has 44,530 entries rather than $10^8$. Every ledger and every quoted count was produced by two programs sharing no code that agree by hash. We record what is known about a non-coalescing pair and measure the exit-set sizes Li bounds. Nothing here is a proof of the conjecture.

arXiv comment6 pages. Lean sources, certificates, ledgers and verification logs at https://github.com/ibrahimmian36/hastatus (release v1)