Lemma 3: the second range reduction, down to
ProvedSidonSqrtN.lemma_3There is an absolute such that any positive integers bounded by , with , reduce to a Sidon-faithful set of at least positive integers with , that is .
Sidon-faithful is written out: reduces to when every Sidon subset of is matched by a Sidon subset of at least as large. Note the direction. A reduct is a set that is no easier, so a lower bound proved for transfers back to .
The bound is squared to stay inside and avoid a real exponent.
import Mathlib
namespace SidonSqrtN
theorem lemma_3 :
∃ c : ℝ, 0 < c ∧ ∀ (A : Finset ℤ) (M : ℕ), (∀ a ∈ A, 0 < a ∧ a ≤ (M : ℤ)) →
M ≤ 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 ^ 2 ≤ (A.card : ℤ) ^ 3) ∧
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 and for all, such that: for every finite set A of integers and every natural number M, if every element of A is strictly positive and at most M, and M is at most |A|^3, then there exists a finite set B of integers with three properties. (i) Every Sidon subset T of B is matched by a Sidon subset S of A with |S| >= |T|; here "Sidon" is spelled out as: for all four elements a,b,c,d of the set, a+b=c+d implies (a=c and b=d) or (a=d and b=c), i.e. the pair {a,b} equals {c,d} as a multiset, with the trivial coincidences allowed. Equivalently (i) says the largest Sidon subset of B is no larger than the largest Sidon subset of A. (ii) Every b in B satisfies 0 < b and b^2 <= |A|^3, i.e. b <= |A|^{3/2}. (iii) |B| >= c|A|, as reals. Nothing requires B to be a subset of A, nor B itself Sidon, nor bounds |B| above; B's only tie to A is through (i), (ii), (iii).
QUANTIFIER ORDER exists c real, c > 0: uniform over all A, M, B; no value given. for all finite A of integers. for all M in N; M occurs only in the hypotheses, never in the conclusion. exists B finite set of integers: chosen after A and M, before T. for all T subset of B (including empty), Sidon. exists S subset of A, Sidon; S may depend on T. Inside the Sidon clauses, a,b,c,d are universally quantified over the set; that inner c shadows the real constant only there, and the final inequality's c is the outer real one.
HYPOTHESES 0 < c strict: rules out c = 0, which would make (iii) vacuous. each a in A: 0 < a strict (no zero, no negatives); a <= M non-strict. M <= |A|^3 non-strict, in N: A cannot be too sparse in [1,M]. Since M is universally quantified and absent from the conclusion, the binding instance is M = max A, so the real content is max A <= |A|^3. No typeclass constraints; all types are concrete.
DEGENERATE CASES A empty: hypotheses force M = 0; B = empty satisfies all three, since c*0 = 0 <= 0. A = {1}: M = 1 and (ii) forces B a subset of {1}, so the statement requires c <= 1. T empty is Sidon vacuously; S empty discharges it. Hypotheses are satisfiable (for example A = {1,...,n}, M = n), so the theorem is not vacuous.
UNREADABLE Nothing untranslated. The body is sorry, so nothing is proved here.
Confirmed by the mission captain (proposal self-audit).