The Exact Extremal Bound in Erdős Problem 848

For N ≥ 1, let A be a subset of [1,N] such that ab+1 is nonsquarefree for every a,b in A, with a=b allowed. We prove the sharp bound |A| ≤ floor((N+18)/25), with equality attained by the elements of the progression 7 modulo 25. Earlier work established the same formula only above a large threshold. Our proof converts the extremal problem, by an exact Hall equivalence, into a completion inequality relative to the progression 7 modulo 25. A prefix-compatible colouring controls all N ≤ 5·10⁶ simultaneously. Beyond this point, square-divisor estimates first eliminate defects supported on the competing progression 18 modulo 25 and then force every remaining defect to contain a large residual set. A valuation and residue decomposition supplies bounded pivot configurations; finite-prime counts and spacing between solutions of a transformed quadratic equation rule out each configuration. The resulting interval estimates are uniform, and a final monotone argument controls the unbounded tail. All finite inequalities and witnesses are exact, and the complete theorem is formally verified in Lean 4.