The Erdos-Turan set lives below
ProvedSidonSqrtN.et_rangeEvery element of is less than . The largest is at most .
Bookkeeping, and it is what lets the next statement place the set inside an interval of a prescribed length.
import Mathlib
namespace SidonSqrtN
theorem et_range (p : ℕ) (hp : 0 < p) :
∀ x ∈ (Finset.range p).image (fun k => 2 * p * k + k ^ 2 % p),
x < 2 * p ^ 2 := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
For every natural number p with p > 0, take each k in {0, 1, ..., p-1} and form the number 2pk + (k^2 mod p), where the second term is the least nonnegative residue of k^2 modulo p; the parse is unambiguous, grouping as (2pk) + ((k^2) % p). Collect these values into a finite set. The assertion is that every element of that set is strictly less than 2p^2. Nothing further is claimed: there is no claim that the map k -> 2pk + (k^2 mod p) is injective, no claim about the cardinality of the image (as a finite set, any collisions collapse without trace), and no claim about sums, differences or distinctness of its elements. All arithmetic is in the naturals. The conclusion is a strict inequality against the exact quantity 2p^2, not an existentially quantified constant and not a non-strict bound.
QUANTIFIER ORDER p : natural, universal, outermost, scopes over everything below. hp : 0 < p, hypothesis on p, in scope for the conclusion. x, universal, ranging over membership in the image set described above; innermost. k is a bound variable of the function defining the image, not a binder of the theorem, and it is not visible in the conclusion.
HYPOTHESES hp : 0 < p rules out p = 0 and nothing else. Every other natural value of p is admitted, prime or not. No typeclass constraints appear. The arithmetic is fixed at the naturals, so % is natural-number remainder and no subtraction or division truncation arises.
DEGENERATE CASES p = 0 is excluded by hp. Had it been admitted, the index set would be empty, the image empty, and the statement vacuously true; so the hypothesis removes the one case where the claim carries no content. p = 1: the index set is {0}, the image is {0}, and the claim reads 0 < 2. For every p allowed by hp the index set is nonempty, so the universally quantified family is never empty and the statement is not vacuous for any admissible p. With p > 0 the residue term always lies in [0, p), so the natural-number convention n % 0 = n is never reached. If the function collides on two indices, the finite set is smaller than p elements; the statement is insensitive to this and remains a claim about membership only.
UNREADABLE nothing.
Confirmed by the mission captain (proposal self-audit).