Remark 3: a small remainder map preserves
ProvedSidonSqrtN.remark_3If every in is written with the remainder small, , then preserves the relation .
The two remainder sums each have absolute value below , so their difference has absolute value below ; it is also a multiple of , so it is zero.
The constant 4 is the paper's for the Sidon relation, whose coefficient vector is . This is the workhorse of every later step of the 1975 route.
import Mathlib
namespace SidonSqrtN
theorem remark_3 (A : Finset ℤ) (q : ℤ) (k r : ℤ → ℤ) (hq : 0 < q)
(hsmall : ∀ a ∈ A, a = k a * q + r a ∧ 4 * |r a| < q) :
IsAddFreimanHom 2 (A : Set ℤ) Set.univ r := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Let A be a finite set of integers, let q be an integer, and let k and r be two functions from the integers to the integers. Assume q > 0. Assume also that every a in A satisfies two conditions at once: a = k(a)*q + r(a), and 4|r(a)| < q. The conclusion asserts that r is an additive Freiman homomorphism of order 2 from A into all of the integers. Unfolding that Mathlib notion at order 2 gives two parts. The first part says r maps A into the universal set, which holds automatically. The second part says that any two multisets of size 2 with entries in A and equal sums have r-images of equal sum. In plain terms, whenever a, b, c, and d lie in A and a + b = c + d, then r(a) + r(b) = r(c) + r(d). Multisets allow repeats, so a = b and c = d are permitted. The functions k and r are arbitrary on all of the integers and are constrained only at points of A; their values elsewhere never enter the conclusion. Nothing forces r(a) to be the usual nonnegative remainder, and nothing forces k(a) to be a floor quotient. The constant 4 is fixed in the statement, and it is not existentially quantified. A carries no hypothesis besides finiteness, and finiteness itself is never used by the conclusion.
QUANTIFIER ORDER A, a finite set of integers, universal, scope is the whole statement. q, an integer, universal, after A. k and r, functions on the integers, universal, after q. hq, then hsmall, both after all four data. Inside hsmall, a universal quantifier over members of A. Inside the conclusion, a universal quantifier over pairs drawn from A with equal sums. No existential quantifier appears anywhere.
HYPOTHESES hq : 0 < q rules out q = 0 and negative q, so the bound 4|r(a)| < q can hold. hsmall, first half, ties r(a) to a modulo q and pins k(a) once r(a) is chosen. hsmall, second half, is strict, so |r(a)| < q/4, and |r(a)| = q/4 is excluded. No typeclass assumptions appear. Everything lives over the integers.
DEGENERATE CASES A empty: hsmall is vacuous, no size-2 multiset draws from A, so the conclusion holds for free. A a singleton: the conclusion reduces to 2r(a) = 2r(a). q at most 4: the bound forces r(a) = 0 for every a in A, and both sides vanish. hsmall is a real restriction on A, not only on k and r: it requires every element of A to lie at distance less than q/4 from a multiple of q. For an A and q where that fails, no k and r exist and the statement is vacuous for that pair.
UNREADABLE Nothing. The proof body is a placeholder, so the file asserts the statement and proves none of it.
Confirmed by the mission captain (proposal self-audit).