An integer-valued Freiman 2-embedding of a finite set of reals

Proved

SidonSqrtN.int_freiman

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

additive-combinatoricscombinatoricsnumber-theory

For every finite set $X$ of reals there is a map $\varphi$ from $\mathbb{R}$ to $\mathbb{Z}$ , injective on $X$ , sending every solution of $a + b = c + d$ in $X$ to a solution of the same equation in $\mathbb{Z}$ .

From the previous statement by clearing denominators: the functional takes finitely many rational values on $X$ , so a single common denominator turns it into an integer-valued map, and scaling a linear map keeps it linear.

Preamble

import Mathlib

Formal statement

namespace SidonSqrtN

theorem int_freiman (X : Finset ℝ) :
    ∃ φ : ℝ → ℤ, Set.InjOn φ (X : Set ℝ) ∧
      IsAddFreimanHom 2 (X : Set ℝ) Set.univ φ := 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

For every finite set X of real numbers there exists a function f from all of the reals to the integers such that f is injective on X and f preserves two-term additive relations inside X: whenever a, b, c, d lie in X and a + b = c + d, then f(a) + f(b) = f(c) + f(d). The second clause is the standard notion of an additive Freiman homomorphism of order 2 from X into the full integer set, which unwinds to two parts. First, f sends X into the universal subset of the integers, which is no restriction at all. Second, for any two multisets drawn from X, each of size exactly 2, with equal sums, the image sums agree; since multisets permit repetition this includes a + a = b + c forcing 2f(a) = f(b) + f(c). Only the forward implication is asserted: equal image sums are never required to force equal sums, so no injectivity of the induced map on sumsets and no isomorphism condition is claimed. The values of f away from X are unconstrained, no bound is placed on the magnitude of f or on the diameter of its image, and no relation is asserted between the size of X and any quantity. The map is chosen after X, so it may depend on X.

QUANTIFIER ORDER

X, a finite set of reals, universal, outermost, scope is the whole statement.
f, a function from the reals to the integers, existential, inside X, may depend on X.
Inside the Freiman clause, an implicit universal over pairs (size-2 multisets) of elements of X with equal sums.

HYPOTHESES X is finite. This rules out infinite sets and nothing else: no cardinality bound, no positivity, no integrality, no separation, no structure. Injectivity is imposed only on the image of X under the coercion to a set, not on the reals. The Freiman target is the universal set of integers, so the "maps into" part of the definition is automatically satisfied and imposes no range restriction. No typeclass constraints beyond the ambient real and integer structures.

DEGENERATE CASES X empty: injectivity is vacuous and there are no qualifying multisets, so any f satisfies the conclusion. X a singleton: the only size-2 multiset is the doubled point, compared with itself, so again any f works. X with no nontrivial additive coincidence (every solution of a + b = c + d has the pair {a,b} equal to {c,d} as a multiset): the Freiman clause is automatic and only injectivity on X remains. No hypothesis is unsatisfiable, so the statement is not vacuous.

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