Erdős Problem 848: A Kernel-Checked Proof of the Exact Extremal Bound

Abstract

For every integer N ≥ 1, the maximum cardinality of a set A contained in [1,N] for which ab+1 is nonsquarefree for every a,b in A is exactly the number of integers n ≤ N with n ≡ 7 (mod 25). The proof uses an exact Hall reformulation, an exact prefix-colouring certificate through 5·106, range compression, valuation-cell-fibre descent, and kernel-certified finite states. The terminal all-N theorem is Erdos848.PaperGeneratedCertificateProvider.all_N and is replayed by the Lean 4 kernel with --trust=0. This version contains the frozen manuscript PDF, its LaTeX source, and the machine-readable proof contract.