A Sidon subset of of size at least
ProvedSidonSqrtN.sidon_in_rangeFor every there is a Sidon set inside with at least elements.
Two regimes. For the fixed set already has three elements and , and for the singleton does. For take and apply Bertrand's postulate to get a prime with . Then , so the previous statement puts the Erdos-Turan set inside the interval, and beats .
Every later milestone pigeonholes a set against this one. It is also the one place in the development where a Sidon set is constructed; everywhere else a Sidon set is found inside something given.
import Mathlib
namespace SidonSqrtN
theorem sidon_in_range (N : ℕ) :
∃ S ⊆ Finset.range N, (∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) ∧
Real.sqrt N / 4 ≤ (S.card : ℝ) := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
For every natural number N, there exists a finite set S of natural numbers contained in {0, 1, ..., N-1} (the first N naturals, N itself excluded) such that two things hold at once. First, S is a Sidon set in the strict sense: whenever a, b, c, d are elements of S, not required to be distinct from one another, and a + b = c + d, then either a = c and b = d, or a = d and b = c. That is, every sum of an ordered pair from S determines the pair up to swapping, so all pairwise sums (including doubles 2a) are distinct apart from the forced coincidence a + b = b + a. Second, the real number sqrt(N)/4 is less than or equal to the cardinality of S, with the cardinality cast to the reals and sqrt the real square root of the cast of N. The constant 1/4 is a literal, not existentially quantified, and the exponent is exactly 1/2. There is no asymptotic clause, no "for sufficiently large N", and no error term: the inequality is asserted for every N with the same constant.
QUANTIFIER ORDER N : natural, universally quantified, outermost; scope is the whole statement. S : finite set of naturals, existentially quantified inside N, so S may depend on N; scope is both conjuncts. a, b, c, d : universally quantified over S, inside the existential, in that order; scope is the implication only. Their order among themselves does not matter here since all four range over the same set.
HYPOTHESES S subset of Finset.range N: bounds every element of S below N, so elements lie in [0, N-1]. It rules out using N or anything larger, and for N = 0 forces S empty. a + b = c + d: the antecedent of the Sidon implication, addition in the naturals (no subtraction or wraparound). Rules out nothing about S by itself; it selects which quadruples must be trivial. No typeclass constraints appear. No hypothesis on N (no positivity, no largeness).
DEGENERATE CASES N = 0: range is empty, so S must be empty; the Sidon clause is vacuous and sqrt(0)/4 = 0 <= 0. Holds trivially. N = 1: S = {0} works; the bound is 0.25 <= 1. 1 <= N <= 16: sqrt(N)/4 <= 1, so any singleton satisfies both clauses, and singletons are Sidon vacuously. The statement carries no content below N = 17. The empty set always satisfies the Sidon clause, so the cardinality bound is the only load-bearing part. No hypothesis is unsatisfiable, and no quantified family is empty except at N = 0.
UNREADABLE Nothing. The payload contains a single declaration with no auxiliary definitions, and every name in it is standard Mathlib vocabulary.
Confirmed by the mission captain (proposal self-audit).