Pull a Sidon set back from the integer image

Proved

SidonSqrtN.sidon_transfer

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

additive-combinatoricscombinatoricsnumber-theory

Given $\varphi$ injective on $X$ and preserving $a + b = c + d$ , any Sidon subset $T$ of the image $\varphi(X)$ comes from a Sidon subset of $X$ of at least the same size, namely its preimage in $X$ .

Only the forward direction of the transfer is ever needed. That is why the embedding is asked to preserve the relation rather than to reflect it.

Preamble

import Mathlib

Formal statement

namespace SidonSqrtN

theorem sidon_transfer (X : Finset ℝ) (φ : ℝ → ℤ) (hinj : Set.InjOn φ (X : Set ℝ))
    (hfre : IsAddFreimanHom 2 (X : Set ℝ) Set.univ φ)
    (T : Finset ℤ) (hT : T ⊆ X.image φ)
    (hTS : ∀ a ∈ T, ∀ b ∈ T, ∀ c ∈ T, ∀ d ∈ T,
      a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) :
    ∃ S ⊆ X, (∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, ∀ d ∈ S,
        a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) ∧
      T.card ≤ S.card := by sorry

end SidonSqrtN

Source

Folklore; the reduction from the reals to the integers in 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

Let X be a finite set of reals and let phi map reals to integers. Assume phi is injective on X, and assume phi is an additive Freiman homomorphism of order 2 from X into all of Z. Unfolded, that second assumption says: for all a, b, c, d in X with a + b = c + d, we get phi(a) + phi(b) = phi(c) + phi(d). Let T be a finite set of integers with T contained in phi(X). Assume T is Sidon in the strong form: whenever a, b, c, d lie in T and a + b = c + d, either a = c and b = d, or a = d and b = c. The four variables are independent, so repeats are covered, and a + a = c + d forces c = d = a. The conclusion asserts the existence of a finite set S of reals with S contained in X, with S Sidon in the identical strong form, and with card T at most card S. The conclusion links S to T only by that cardinality inequality. It does not ask that phi map S onto T, nor that S meet the preimage of T at all.

QUANTIFIER ORDER X, a finite set of reals: universal, outermost. phi, total on R: universal, constrained only on X. T, a finite set of integers: universal, after phi. S: existential, may depend on X, phi and T. a, b, c, d in T and in S: universal, independent, repeats allowed.

HYPOTHESES Injectivity on X: rules out two distinct points of X with a common phi value. Says nothing off X. Freiman 2-hom: preserves additive quadruples forward, from X into Z. The converse direction is not asserted, so equal sums in the image need not come from equal sums in X. The codomain set is all of Z, so the mapping part of that condition is automatic. T inside phi(X): rules out integers of T outside the image of X. T Sidon: rules out every nontrivial coincidence a + b = c + d inside T.

DEGENERATE CASES T empty: conclusion holds with S empty, since the Sidon condition is vacuous there and 0 <= 0. X empty: forces T empty, same reading. T a singleton: any singleton subset of X satisfies the conclusion. Hypotheses are jointly satisfiable and nonvacuous. Take X a finite set of integers sitting in R and phi the floor function. No constant, exponent or growth rate appears anywhere in the statement.

UNREADABLE Nothing. The only nonstandard item is the Mathlib Freiman homomorphism predicate, whose order-2 case I expanded above from its multiset definition.

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