A Sidon subset of maximum cardinality exists
ProvedSidonSqrtN.max_sidon_existsEvery finite set of reals has a Sidon subset no smaller than any other Sidon subset.
There are finitely many subsets, so this is extremality on a finite nonempty family, the empty set being always available. Short, and it is what makes "take a maximal Sidon subset" a legal move in the next statement.
import Mathlib
namespace SidonSqrtN
theorem max_sidon_exists (X : Finset ℝ) :
∃ S ⊆ X, (∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) ∧
∀ T ⊆ X, (∀ a ∈ T, ∀ b ∈ T, ∀ c ∈ T, ∀ d ∈ T,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) → T.card ≤ S.card := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
For every finite set X of real numbers there exists a subset S of X such that: whenever a, b, c, d all belong to S and a + b = c + d, either a = c and b = d, or a = d and b = c; and S has maximum size among all subsets of X with that same property, meaning every subset T of X satisfying the identical condition has |T| <= |S|. Because a, b, c, d range independently over the subset, repetitions are permitted, so the condition also forbids x + y = 2z for three distinct elements: it says all pairwise sums with repetition allowed are distinct except for the forced swap. The assertion is exactly the existence of a maximum-cardinality subset of this kind. No numerical bound on |S| is stated anywhere: no square root of |X|, no constant, no exponent, no asymptotics. The elements are arbitrary reals, with no integrality, positivity, ordering or range restriction, and no condition on |X|.
QUANTIFIER ORDER X: universally quantified, a finite set of reals; scope is the whole statement. S: existentially quantified after X, so S may depend on X; scope is the conjunction that follows. a, b, c, d in the first condition: universally quantified over S, independently, repeats allowed; scope is one implication. T: universally quantified inside the scope of S, so the chosen S must beat every such T; scope is the final inequality. a, b, c, d in the second condition: universally quantified over T, independently, repeats allowed.
HYPOTHESES X is a finite set (Finset), which rules out infinite collections and makes the cardinality comparison meaningful. S is a subset of X (not necessarily proper, not necessarily nonempty). T is a subset of X (not necessarily proper, not necessarily nonempty). The sum-distinctness condition on T is the antecedent of the cardinality bound, so it rules out comparison with subsets that fail the condition. No typeclass constraints beyond the ambient real numbers. No hypothesis is unsatisfiable.
DEGENERATE CASES X empty: S = empty set works; the condition is vacuous and the only T is empty, so 0 <= 0. The empty set and every singleton satisfy the condition, and so does every two-element set (a + b = c + d with a, b, c, d drawn from two elements always forces one of the two disjuncts), so the family of admissible T is never empty and S is nonempty whenever X is. S is not claimed unique, and nothing forces S to be a proper subset; if X itself satisfies the condition then S = X is allowed. Three-element sets can fail, for instance {0, 1, 2} via 0 + 2 = 1 + 1, so the condition has content.
UNREADABLE Nothing. The payload contains a single declaration with no auxiliary definitions, and every predicate is written out inline.
Confirmed by the mission captain (proposal self-audit).