The Erdos-Turan set has exactly $p$ elements

Proved

SidonSqrtN.et_card

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatoricsnumber-theory

The set $\{2pk + (k^2 \bmod p) : 0 \le k < p\}$ has exactly $p$ elements.

The defining map is injective on $\{0, \dots, p-1\}$ . Since $k^2 \bmod p$ is below $p$ , and $p \le 2p$ , the value $2pk + (k^2 \bmod p)$ determines $k$ as its quotient by $2p$ . Primality is not needed here, only $p > 0$ .

Preamble

import Mathlib

Formal statement

namespace SidonSqrtN

theorem et_card (p : ℕ) (hp : 0 < p) :
    ((Finset.range p).image (fun k => 2 * p * k + k ^ 2 % p)).card = p := by sorry

end SidonSqrtN

Source

Paul Erdos and Pal Turan, "On a problem of Sidon in additive number theory, and on some related problems", J. London Math. Soc. 16 (1941) 212-215

Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

For every natural number p with p at least 1, take the p numbers k = 0, 1, ..., p-1, and for each form the natural number 2pk + (k^2 mod p). Collect those p values into a finite set, which merges any repeats. The assertion is that this set has exactly p elements, equivalently that the map k -> 2pk + (k^2 mod p) is injective on {0, 1, ..., p-1}. Everything is in the naturals: mod is the remainder of k^2 on division by p, the exponent is exactly 2, the product parses as (2p) times k, and the remainder term is added afterwards. Since p > 0, the remainder lies in [0, p), so each value is a multiple of 2p plus an offset strictly smaller than p, hence strictly smaller than the spacing 2p between consecutive multiples. The equality of cardinalities therefore records only that distinct k give distinct multiples 2pk with non-overlapping offset windows. It says nothing about which residues k^2 mod p occur, nothing about whether two different k share a residue, and nothing about sums or differences of the listed values. The count p is exact, not a bound, and there is no constant or exponent left free anywhere.

QUANTIFIER ORDER p : natural number, universally quantified, scope is the hypothesis and the whole conclusion. hp : the hypothesis 0 < p, in scope for the conclusion. k : bound by the function inside the image operation, ranging over the p values 0 through p-1; its scope is the single expression 2pk + (k^2 mod p) and it is not visible outside. No existential quantifier appears.

HYPOTHESES hp : 0 < p rules out p = 0 only. It is satisfiable for every p >= 1, so the statement is not vacuous and the family it quantifies over is infinite. No typeclass constraint appears; the only type is the naturals, with their truncated arithmetic and Euclidean remainder. There is no primality, oddness, or coprimality assumption on p, and no auxiliary declaration in the payload.

DEGENERATE CASES p = 0 is excluded by hp. Had it been allowed, the index set would be empty, the image empty, and both sides would be 0. p = 1: the index set is {0}, the single value is 0, and the count is 1. For any p, if p were composite or even, the statement is unchanged, since no hypothesis distinguishes those cases. The quantified family is never empty and no hypothesis is unsatisfiable.

UNREADABLE nothing. The payload contains one declaration and no auxiliaries; its proof body is omitted.

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by aarontcao · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Erdos-Turan set has exactly ppp elements

The Erdos-Turan set has exactly $p$ elements