The Eventual Four-Divisor Bound for Erdős Problem 887: Root-band Reconstruction and a K5 Interval-Overload Obstruction

This record contains a preprint manuscript presenting a proof of Erdős Problem 887. The manuscript proves an eventual four-divisor bound for the fourth-root near-root divisor window. For each fixed constant C > 0, it proves that there is a threshold N(C) such that the interval (sqrt(n), sqrt(n) + C n^(1/4)) contains at most four divisors of n for all n >= N(C). The proof is organized around two reductions. The external reconstruction reduction turns an unbounded sequence of five-divisor violations into a normalized legal five-endpoint K5 survivor carrying a canonical interval-overload datum. The internal obstruction proves that no such canonical interval-overload datum exists. A companion Lean 4 formalization is archived separately and mirrors the theorem-source architecture of the manuscript.