Some translate of meets in points
ProvedSidonSqrtN.translate_averagingFor and inside , some translate meets in at least points. Double counting over all translates.
This stands in for Singer's 1938 covering of by Sidon sets, which the published proof uses and which is not available here. It does the same job at the same order, since a Sidon set of size about averaged over translates meets a set of size in about points. The constant comes out worse than Singer's , and the goal only claims that some exists.
import Mathlib
namespace SidonSqrtN
theorem translate_averaging (m : ℕ) [NeZero m] (A B : Finset (ZMod m)) :
∃ i : ZMod m,
(A.card * B.card : ℝ) / m ≤ (((B.image (· + i)) ∩ A).card : ℝ) := by sorry
end SidonSqrtN
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Fix a natural number m that is nonzero, and work in the additive group Z/mZ, which then has exactly m elements. Let A and B be finite subsets of that group. The statement asserts that some element i of Z/mZ exists for which the translate B + i = {b + i : b in B} meets A in at least |A| |B| / m elements. The right side is the cardinality of the intersection of the translated set with A, cast to a real number. The left side is a real division of the product of the two cardinalities by m. The inequality is non-strict, and the constant is exactly 1, with no slack factor and no error term. Translation is injective, so the intersection count equals the number of pairs (a, b) in A x B with a = b + i, and summing that count over all i gives |A| |B|. The bound named is therefore the mean of the counts over the m translates. No explicit i is produced; only its existence is claimed.
QUANTIFIER ORDER m natural, universal, outermost. NeZero m, an instance constraint on m. A, B finite subsets of Z/mZ, universal, independent of each other. i in Z/mZ, existential, innermost, so it may depend on m, A, and B.
HYPOTHESES NeZero m rules out m = 0. That matters twice: ZMod 0 is the integers, which is infinite, and division by zero returns zero in Lean, which would flatten the bound to 0 <= count. Nothing is assumed about A and B. They may be empty, equal, disjoint, singletons, or the whole group, and no bound relates their sizes to m. Decidable equality on Z/mZ, needed to form the intersection, is standard and carries no content.
DEGENERATE CASES A empty or B empty: the left side is 0 and the intersection is empty, so the claim reads 0 <= 0 and holds for every i. m = 1: the group is trivial and every translate of B equals B, so the claim reads |A| |B| <= |A and B| with both cardinalities at most 1. A = B = the whole group: both sides equal m for every choice of i. No hypothesis is unsatisfiable, and the family of instances is nonempty, so the statement is not vacuous.
UNREADABLE Nothing. The payload is a single declaration with the proof left as sorry, and it carries no auxiliary declarations.
Confirmed by the mission captain (proposal self-audit).