Lemma 5: any positive integers compress into
ProvedSidonSqrtN.lemma_5There is an absolute such that any positive integers reduce to a Sidon-faithful set of at least positive integers all at most .
The assembly calls this statement and no other part of the 1975 chain. The paper's constant is , which is for the Sidon relation. It is left existential here because that numeral was read off a rough scan, and a statement signed with a constant slightly too strong can never be proved.
import Mathlib
namespace SidonSqrtN
theorem lemma_5 :
∃ c : ℝ, 0 < c ∧ ∀ A : Finset ℤ, (∀ a ∈ A, 0 < a) →
∃ 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
One real constant c > 0 is fixed first and serves every case. Then for every finite set A of integers whose elements are all strictly positive, there is a finite set B of integers with three properties. (i) Every Sidon subset of B is matched inside A: for each T contained in B such that all a,b,c,d in T with a+b=c+d satisfy (a=c and b=d) or (a=d and b=c), there is an S contained in A with that same property and |T| <= |S|. S is otherwise unconstrained, with no tie to T beyond cardinality. (ii) Every b in B satisfies 1 <= b <= |A|. (iii) c*|A| <= |B|. So B lies in the integer interval [1,|A|], holds at least a fixed positive proportion of |A| elements, and its largest Sidon subset is no larger than A's. B need not meet A at all.
QUANTIFIER ORDER exists c : R, outermost, uniform over all A. for all A : Finset Z, under the positivity hypothesis. exists B : Finset Z, may depend on A and c. for all T contained in B, then the Sidon premise on T, then exists S contained in A (may depend on T), then Sidon on S and |T| <= |S|. Shadowing: the letter c is reused as a bound integer inside both Sidon formulas. The final inequality sits outside those binders, so there c is the real constant.
HYPOTHESES 0 < c: excludes c = 0, which would drain clause (iii). for all a in A, 0 < a: A is a set of positive integers with no upper bound, so it may be arbitrarily spread out. Sidon premise on T: non-Sidon subsets of B impose no obligation. 0 < b and b <= |A| for b in B: confines B to {1,...,|A|}, so |B| <= |A| for free and (iii) is a lower bound only. It also forces c <= 1 once one nonempty A exists. No typeclass hypotheses; ambient types are Z and R.
DEGENERATE CASES A empty: positivity holds vacuously, |A| = 0, no b satisfies 0 < b <= 0, so B empty is forced and all three clauses hold. T empty is always admissible and is discharged by S empty. |A| = 1: c > 0 forces B nonempty, so B = {1}. Nothing vacuous: every hypothesis is satisfiable, so the claim has content for each A. Cardinalities are naturals cast into Z and R, with no truncated subtraction.
UNREADABLE nothing. No auxiliary declarations and no local definitions; the Sidon condition is written out in full at both occurrences. The proof body is a placeholder, so the payload asserts the statement without establishing it.
Confirmed by the mission captain (proposal self-audit).