A $\mathbb{Q}$ -linear functional injective on a finite set of reals

Proved

SidonSqrtN.q_separator

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

additive-combinatoricscombinatoricsnumber-theory

For every finite set $X$ of reals there is a $\mathbb{Q}$ -linear map from $\mathbb{R}$ to $\mathbb{Q}$ that is injective on $X$ .

$X$ is finite, so its $\mathbb{Q}$ -span is finite dimensional. Pick a basis, and take the functional whose value is the coordinate vector read as an integer in base $M$ , for $M$ past every coordinate difference. Extend to all of $\mathbb{R}$ by a Hamel basis, which is where the axiom of choice enters.

Preamble

import Mathlib

Formal statement

namespace SidonSqrtN

theorem q_separator (X : Finset ℝ) :
    ∃ f : ℝ →ₗ[ℚ] ℚ, Set.InjOn f (X : Set ℝ) := 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 Q-linear map f from R to Q, where R and Q are both regarded as vector spaces over the rationals, such that f is injective on X. Injectivity on X means: for all a and b belonging to X, if f(a) = f(b) then a = b. Equivalently, f takes |X| distinct rational values on X. The map f is bundled with its linearity, so f(a + b) = f(a) + f(b) for all real a and b, and f(q a) = q f(a) for every rational q; those identities hold on all of R, not only on X. The only condition imposed on f beyond linearity is injectivity on the points of X itself. Nothing is asserted about the images of sums, differences or other combinations of elements of X, about f being nonzero, about the size of the values f(x), or about f being injective anywhere outside X. The proof body is a placeholder (sorry), so the payload carries a statement only, with no auxiliary declarations.

QUANTIFIER ORDER

X, a finite set of reals: universal, outermost, scopes over everything below.
f, a Q-linear map R -> Q: existential, inside X, so f is allowed to depend on X. This is not a single f serving all finite sets at once.
a and b, elements of X: universal, innermost, hidden inside the injectivity-on-a-set predicate, with the hypothesis f(a) = f(b) and conclusion a = b.

HYPOTHESES X is a finite set. This rules out infinite X, and it is the only substantive assumption. Elements of X may be zero, negative, rational, or rationally dependent in any way; there is no independence, positivity, separation or cardinality condition. A finite set carries no repeated elements by construction. The typeclass content is implicit in the notation for a Q-linear map: canonical Q-module structures on R and on Q, resolved automatically. They exclude nothing. The coercion of X to a set of reals is just its underlying set; it adds no condition.

DEGENERATE CASES X empty: the injectivity condition is vacuous, so any linear map witnesses it, including the zero map. The statement holds with no content there. X a singleton: same, the only pair is a = b. For X with at least two elements the zero map fails the condition, so a witness must be nonconstant on X. No hypothesis is unsatisfiable, and the universally quantified family of finite sets is nonempty, so the statement is not vacuous overall.

UNREADABLE Nothing. Every symbol in the payload translated.

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

A Q\mathbb{Q}Q-linear functional injective on a finite set of reals

A $\mathbb{Q}$ -linear functional injective on a finite set of reals