Erdős Problem 848: Exact Hall Closure by Square-Sieve Descent and Prefix Colouring

For N ≥ 1, let A ⊆ [1,N] have the property that ab+1 is nonsquarefree for every a,b ∈ A. We prove that |A| is at most the number of integers n ≤ N with n ≡ 7 (mod 25), with equality attained by the progression 7 (mod 25). The proof rewrites the assertion as an exact Hall inequality, establishes the finite ranges by exact prefix colouring and finite square-sieve arguments, and proves the remaining tail by valuation-cell-fibre descent. All finite enumerations use integer or rational arithmetic; their semantic checkers and the terminal all-N theorem are replayed by the ordinary Lean kernel.