The Komlos-Sulyok-Szemeredi bound: a Sidon subset of size
ProvedSidonSqrtN.sidon_subset_sqrtThere is an absolute constant such that every finite set of positive reals contains a subset all of whose pairwise sums are distinct, with .
A set with all pairwise sums distinct is a Sidon set. The condition is written out at each use: for with , either and , or and . Repeats are allowed on both sides, so is not excluded; what is excluded is two genuinely different unordered pairs sharing a sum.
The constant is quantified outside the , so it is absolute and there is no "for large enough" escape hatch. Small is covered by taking small, since a one-element set is Sidon. Positivity of the elements is never used, because the Sidon condition is translation invariant; it stays because the problem states it.
import Mathlib
namespace SidonSqrtN
theorem sidon_subset_sqrt :
∃ c : ℝ, 0 < c ∧ ∀ X : Finset ℝ, (∀ x ∈ X, 0 < x) →
∃ S ⊆ X, (∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) ∧
c * Real.sqrt X.card ≤ (S.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 for all, such that: for every finite set X of real numbers whose elements are all strictly positive, there exists a subset S of X with two properties. First, for all a, b, c, d in S, if a + b = c + d then either (a = c and b = d) or (a = d and b = c); that is, the only coincidences among two-element sums from S are the forced ones, so all sums a + b with a, b in S determine the unordered pair. Second, c times the square root of the number of elements of X is less than or equal to the number of elements of S. The letter c is reused: inside the sum condition it names an element of S, but that binder closes with the parenthesis, so the c in the final inequality is the outer constant. Exponent is exactly 1/2 on |X|, the constant is a single unspecified positive real rather than a named value, the inequality is non-strict, and there is no additive or logarithmic term.
QUANTIFIER ORDER exists c real, scope: the whole statement 0 < c for all X, a finite set of reals, scope: the implication hypothesis on X, then: exists S with S subset of X, scope: the conjunction inside conjunct one only: for all a, then b, then c, then d in S
HYPOTHESES 0 < c: rules out c = 0, which would make the bound trivial since S empty satisfies everything. every element of X is strictly positive: rules out 0 and negative entries. Nothing is asserted about sets meeting those. Elements are arbitrary reals, not restricted to integers or rationals. S subset of X: not proper, so S = X is permitted. The sum condition places no distinctness requirement on a, b, c, d and holds for any set of size at most 2. X is a finite set, so its elements are pairwise distinct and |X| counts them.
DEGENERATE CASES X empty: hypothesis vacuous, take S empty, both sides are 0, holds for every c. This case constrains nothing. |X| = 1: forces c at most 1, so the statement is false for any c above 1. Small |X|: every one- or two-element subset satisfies the sum condition, so small cases only cap c from above. A fixed finite S cannot work as |X| grows, so the content is the growth rate, not any single instance. The square root is applied to the cast of a cardinality, which is never negative, so no out-of-domain branch arises. The bound forces S nonempty whenever X is nonempty.
UNREADABLE nothing
Confirmed by the mission captain (proposal self-audit).