Erdős-Turán Additive Bases Conjecture

This preprint provides an exhaustive mathematical treatise on the Erdős-Turán Additive Bases Conjecture (Problem #16 / #142 in Paul Erdős' collection, 1941), one of the deepest open problems in additive number theory and asymptotic combinatorics. The conjecture asserts that if a subset A ⊆ ℕ is an asymptotic additive basis of order 2 (meaning that every sufficiently large integer n ≥ n0 can be written as n = a + b with a, b ∈ A), then its representation counting function rA(n) = #{(a, b) ∈ A2 ∣ a + b = n} cannot remain uniformly bounded: limsupn → ∞ rA(n) = ∞ This treatise provides an analytical and combinatorial survey of Erdős's classical 1956 probabilistic construction of a Θ(log n) basis, generating function singularities on the unit disc, and the structural impossibility of Sidon sets forming asymptotic bases. Key Mathematical Results & Contributions Erdős's Probabilistic Basis Theorem (1956): Detailed exposition of the existence of an additive basis satisfying c1 log n ≤ rA(n) ≤ c2 log n via independent random selections with probability px = C √{(log x)/x} and Chernoff concentration bounds. Generating Function Singularity Analysis: Examination of the analytic convolution F(z)2 = ∑n=0∞ rA(n) zn on the complex unit disc 𝔻 and the boundary divergence as z → 1−. Sidon Set Density Barrier: Complete algebraic proof that no Sidon set (B2 set with rA(n) ≤ 2) can ever form an additive basis due to the parabolic counting constraint |A ∩ [1, N]| ≤ √N + O(N1/4). Additive Energy Bounds & Cauchy-Schwarz: Structural connections between representation variance ∑ rA(n)2 and additive quadruples. 100% Machine-Checked Verification in Lean 4: Additive basis predicates, finite representation counting functions, representation sum identities, and Sidon non-basis impossibility are machine-certified with 0 axioms, 0 linter warnings, and 0 sorry placeholders via the Lean 4 interactive theorem prover and Mathlib. Repository and Verification Artifacts The companion machine-checked code and formal verification artifacts are publicly hosted on GitHub:https://github.com/flouzzy/erdos-problemsInteractive Portal: https://maths-proofs.edounze.com/#erdos-16-turan Primary MSC (2020): 11B13, 11B34, 11P70, 68V20, 05D40.