Bailleul-Riblet Lemma 2.3: compression by a real rotation parameter

Proved

SidonSqrtN.compression

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

additive-combinatoricscombinatoricsnumber-theory

For any finite set $A$ of integers and any positive $m$ , there is a subset $C$ of $A$ with at least $|A|/2 - |A|^2/(2m)$ elements carrying a map into $\mathbb{Z}/m\mathbb{Z}$ that is injective on $C$ and preserves $a + b = c + d$ .

Put $\varphi_\theta(a) = \lfloor am\theta \rfloor \bmod m$ and keep $B_\theta = \{a \in A : \{am\theta\} < 1/2\}$ . On $B_\theta$ two fractional parts sum to less than one, so no carry occurs and $\varphi_\theta$ is additive. Multiplication by a nonzero integer preserves Lebesgue measure mod one, so the average of $|B_\theta|$ over $\theta \in [0,1)$ is at least $|A|/2$ , while each colliding pair contributes at most $1/m$ . Choose a $\theta$ beating both averages, then delete one element from each colliding pair.

Taking $m$ of order $n$ makes the bound a constant fraction of $n$ . The 1975 route reaches the same place through four lemmas and a prime counting bound, and this one statement replaces all of them.

Preamble

import Mathlib

Formal statement

namespace SidonSqrtN

theorem compression (A : Finset ℤ) (m : ℕ) (hm : 0 < m) :
    ∃ C ⊆ A, ∃ φ : ℤ → ZMod m,
      Set.InjOn φ (C : Set ℤ) ∧
      IsAddFreimanHom 2 (C : Set ℤ) Set.univ φ ∧
      (A.card : ℝ) / 2 - (A.card : ℝ) ^ 2 / (2 * m) ≤ (C.card : ℝ) := by sorry

end SidonSqrtN

Source

Bailleul and Riblet, arXiv:2605.03181, https://arxiv.org/abs/2605.03181, Lemma 2.3

Read-back

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

READ-BACK

For every finite set A of integers and every positive natural number m, there exist a subset C of A and a function phi from the integers to Z/mZ such that phi is injective on C, phi is an additive Freiman homomorphism of order 2 from C into all of Z/mZ (whenever a, b, c, d lie in C, repetitions allowed, with a + b = c + d, one has phi(a) + phi(b) = phi(c) + phi(d) in Z/mZ), and the real number |A|/2 - |A|^2/(2m) is at most |C|. Both terms of the bound are built from |A|, with exponent exactly 2 in the second and the exact constants 1/2 and 1/(2m). phi is an arbitrary function, not required to be reduction mod m and not constrained anywhere outside pairs drawn from C. The Freiman condition is one directional: equal pairwise sums in C force equal sums of images, while phi(a) + phi(b) = phi(c) + phi(d) is permitted without a + b = c + d. The stated codomain is all of Z/mZ, so the "maps into" half of the Freiman condition carries no information.

QUANTIFIER ORDER A, finite set of integers, universal, outermost. m, natural number, universal. hm, a proof that m > 0. C, finite set of integers, existential, may depend on A and m, constrained by C contained in A, not proper. phi, function from Z to Z/mZ, existential, chosen after C so it may depend on C.

HYPOTHESES hm : 0 < m rules out m = 0, where Z/mZ would be the full integers, and keeps the division by 2m meaningful. No hypothesis at all on A beyond being finite: no size bound, no condition on its sums or differences, no sign or spacing condition. No typeclass constraint is written; the Z/mZ instances are the standard ones.

DEGENERATE CASES C empty satisfies both non-numeric conjuncts vacuously (injective on the empty set, no pairs to test), so the whole content of the claim sits in the cardinality bound. If |A| >= m the right side is at most 0, so C empty discharges the claim. Content exists only when |A| < m. A empty gives 0 <= |C|. m = 1 makes Z/mZ a single point, so injectivity forces |C| <= 1, and the bound is at most 0 for every |A|. Injectivity into a set of size m forces |C| <= m throughout; the demanded quantity never exceeds m/8, its value at |A| = m/2.

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