Maximality forces
ProvedSidonSqrtN.max_sidon_cubeIf is a Sidon subset of of maximum size, then .
Adding any outside must break the Sidon property, and since itself is Sidon the broken relation has to involve . Either with , so , at most values, or , so , at most values. With the elements of that gives , the last step needing , which holds unless is empty.
import Mathlib
namespace SidonSqrtN
theorem max_sidon_cube (X S : Finset ℝ) (hSX : S ⊆ X)
(hS : ∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c))
(hmax : ∀ 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) :
X.card ≤ 3 * S.card ^ 3 := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Let X and S be finite sets of real numbers with S contained in X (containment non-strict). Assume S is a Sidon set: for any four elements a, b, c, d of S, not required distinct, with a + b = c + d, either a = c and b = d, or a = d and b = c. Assume also that S is of maximum size among Sidon subsets of X: every T contained in X satisfying that same four-variable condition has |T| at most |S|. The conclusion is |X| <= 3 |S|^3. The constant 3 and the exponent 3 are both fixed literals, not existentially quantified. Equivalently, |S| >= (|X|/3)^(1/3), a cube-root lower bound on a maximum Sidon subset. No structure is imposed on X beyond finiteness: no integrality, no interval, no separation, no bound on its diameter. Nothing is claimed in the reverse direction.
QUANTIFIER ORDER X: finite subset of R, universal, outermost. S: finite subset of R, universal, second. Inside hS: a, b, c, d universal over S, mutually independent. Inside hmax: T universal over subsets of X, then a, b, c, d universal over T. No existential binder anywhere; the conclusion is quantifier-free.
HYPOTHESES hSX: S subset of X, non-strict, so S = X is permitted. hS: rules out any coincidence among pairwise sums of S other than the trivial swap. It includes the instances a = b and c = d, so a + a = c + c forces a = c (automatic in R). hmax: maximality of |S| among Sidon subsets of X. Instantiated at a singleton it forces |S| >= 1 whenever X is nonempty; instantiated at the empty set it says nothing. It does not itself assert S is Sidon (hS does that), and it does not make S unique. No typeclass constraints appear. Only addition on R is used; the order on R enters only in the final cardinality inequality.
DEGENERATE CASES X empty: S is then empty and the conclusion reads 0 <= 0. S empty with X nonempty: hmax fails against a singleton T, so this cannot arise. Whenever the hypotheses hold with X nonempty, |S| >= 1 and the bound reads |X| <= 3. |S| = 1: every 2-element subset of R is Sidon, so hmax forces |X| <= 1, well inside the stated bound. The hypotheses are satisfiable, so the statement is not vacuous. For instance X = {0, 1, 2, 3} with S = {0, 1, 3} satisfies all three, and the claim reads 4 <= 81.
UNREADABLE Nothing. Every binder and hypothesis translated. The proof body is sorry, so the payload carries the statement only, and there are no auxiliary declarations.
Confirmed by the mission captain (proposal self-audit).