Prove2Me

The cube-root bound: a Sidon subset of size c∣X∣1/3c|X|^{1/3}

Proved
SidonSqrtN.sidon_cbrt

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatoricsnumber-theory

There is an absolute c>0c > 0 such that every finite set of reals has a Sidon subset of size at least c∣X∣1/3c|X|^{1/3}. Immediate from the previous two with c=3−1/3c = 3^{-1/3}.

This is the ceiling for any purely probabilistic argument, because an arithmetic progression of length nn really does have additive energy of order n3n^3. Getting from 1/31/3 to 1/21/2 is the whole problem.

Preamble
import Mathlib
Formal statement
namespace SidonSqrtN

theorem sidon_cbrt :
    ∃ c : ℝ, 0 < c ∧ ∀ X : Finset ℝ,
      ∃ S ⊆ X, (∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
          a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) ∧
        c * (X.card : ℝ) ^ ((1 : ℝ) / 3) ≤ (S.card : ℝ) := by sorry

end SidonSqrtN
Source
The cube-root bound is folklore; see the introduction of Janos Komlos, Miklos Sulyok, and Endre Szemeredi, "Linear problems in combinatorial number theory", Acta Math. Acad. Sci. Hungar. 26 (1975) 113-121
Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

There exists a strictly positive real constant, fixed once and for all, such that every finite set X of real numbers has a subset S which is a Sidon set and satisfies |S| >= c * |X|^(1/3). "Sidon" is spelled out inline: for all a, b, c', d in S, each ranging independently over S with repeats allowed, a + b = c' + d implies (a = c' and b = d) or (a = d and b = c'). The exponent 1/3 is a real exponent applied to a real base, so the right side is the real cube root of the cardinality, and the inequality is non-strict. X ranges over finite sets of arbitrary reals, not integers and not an initial interval. The declaration carries no proof.

Scoping note: the Sidon clause rebinds the name c as one of its four bound variables. That rebinding ends at the closing parenthesis of the Sidon clause, so the c multiplying |X|^(1/3) is the outer existential constant, not a set element.

QUANTIFIER ORDER

  1. Exists c real. Scope: the whole rest of the statement, so c is uniform over all X.
  2. 0 < c.
  3. For all X, a finite set of reals. Scope: everything after.
  4. Exists S, a finite set of reals, with S subset of X. May depend on X.
  5. Inside the first conjunct only: for all a, b, c', d in S, four independent binders.

HYPOTHESES 0 < c: rules out c = 0 and c negative, either of which would make the cardinality bound automatic. S subset of X: ordinary subset, not proper. S = X and S empty are both permitted. No condition on X whatsoever: no lower bound on |X|, no integrality, no spacing, no genericity. The Sidon property is asserted about S, not assumed. The four binders are independent, so collapsed instances count: taking a = b forces 2a = c' + d to give c' = d = a. No typeclass constraints beyond the ambient real field.

DEGENERATE CASES X empty: take S empty. The Sidon clause is vacuous and the bound reads c * 0^(1/3) = 0 <= 0, since the rpow convention sends 0 to 0 for a nonzero exponent. Holds. |X| = 1: 1^(1/3) = 1, so the instance demands c <= 1. Singletons are Sidon, so this pins the constant to at most 1 without being unsatisfiable. |X| = 2: any two-element set satisfies the Sidon clause, checked directly through the second disjunct. Nothing is vacuous. No hypothesis is unsatisfiable and the quantified family of X is nonempty. The constant is existentially bound, so no numeric value is claimed for it.

UNREADABLE nothing

Human review

  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by aarontcao · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph