Lemma 4: the third range reduction, down to
ProvedSidonSqrtN.lemma_4There is an absolute such that any positive integers bounded by reduce to a Sidon-faithful set of at least positive integers bounded by .
The paper's bound is , which for the Sidon relation is , so is the weaker requirement and the statement stays true as written.
import Mathlib
namespace SidonSqrtN
theorem lemma_4 :
∃ c : ℝ, 0 < c ∧ ∀ (A : Finset ℤ) (M : ℕ), (∀ a ∈ A, 0 < a ∧ a ≤ (M : ℤ)) →
(M : ℤ) ^ 2 ≤ (A.card : ℤ) ^ 3 →
∃ B : Finset ℤ,
(∀ T ⊆ B, (∀ a ∈ T, ∀ b ∈ T, ∀ c ∈ T, ∀ d ∈ T,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) →
∃ S ⊆ A, (∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) ∧
T.card ≤ S.card) ∧
(∀ b ∈ B, 0 < b ∧ b ≤ (A.card : ℤ)) ∧
c * A.card ≤ (B.card : ℝ) := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
There is a positive real constant c, fixed once before everything else, such that for every finite set A of integers and every natural number M the following holds. Assume every element of A lies in [1, M], and assume M^2 <= |A|^3. Then there exists a finite set B of integers with three properties. First: every subset T of B that is a Sidon set (whenever a+b = c+d with a, b, c, d in T, either a = c and b = d, or a = d and b = c) admits a Sidon subset S of A with |T| <= |S|. S is required to bear no other relation to T. So this clause says the largest Sidon subset of B is no larger than the largest Sidon subset of A. Second: every element of B lies in [1, |A|], the bound being |A| and not M. Third: c * |A| <= |B|. No rate, exponent or numeric value for c appears anywhere; c is only asserted to exist and be positive.
QUANTIFIER ORDER exists c real, positive: scope is the entire statement, so c is uniform in A and M. for all A, a finite set of integers; then for all M natural. two hypotheses on A and M (below). exists B, a finite set of integers, depending on A and M. within B's first property: for all T subset of B, then exists S subset of A, chosen after T.
HYPOTHESES Membership: each a in A satisfies 0 < a and a <= M. Rules out zero, negatives, and anything exceeding M. Forces |A| <= M, and forces A empty when M = 0. Density: M^2 <= |A|^3, stated over the integers. Rules out A being sparse in [1, M]; it gives |A| >= M^(2/3). No typeclass constraints appear. A, B, S, T are finite sets of integers, so elements are distinct and cardinalities are plain counts.
DEGENERATE CASES A empty: the density hypothesis becomes M^2 <= 0, so M = 0, and B empty satisfies all three clauses, since c * 0 <= 0. T empty is Sidon, and S empty answers it. For A nonempty, c > 0 forces B nonempty. Since B is contained in [1, |A|], we get |B| <= |A|, so any nonempty A forces the witness c to be at most 1. The hypotheses are satisfiable, for instance M = 1 with A = {1}, so the statement is not vacuous. Name shadowing: the real constant c is shadowed by the bound variable c inside both Sidon conditions. The c in the final inequality sits outside those binders and is the real constant.
UNREADABLE Nothing. Every binder translated. The declaration body is a placeholder, so the payload carries a statement and no proof.
Confirmed by the mission captain (proposal self-audit).