A Second-Logarithm Lower Bound for Sets with No Unique Sums
Jiao-Long Cao, Ye Yuan
math.CO
Aug 7, 2026 · v1
TL;DR
All headline statements and structural implications are verified in Lean 4 with explicit integer constants.
Abstract
For an odd prime $p$, let $m(p)$ be the minimum cardinality of a set $A\subseteq \mathbb Z/p\mathbb Z$, with $|A|\geq2$, such that no sum in $A+A$ has a unique representation as an unordered pair from $A$, with repetition allowed. Bedert proved \[ m(p)\gg \log p\, \frac{\sqrt{\log^{(3)}p}}{\log^{(4)}p}. \] We prove the stronger lower bound \[ m(p)\gg \log p\,\log\log p. \] More generally, if $G$ is a finite Abelian group and $q(G)$ is the least prime divisor of $|G|$, then the same explicit estimate holds whenever $q(G)>2$, and in particular every subset $A\subseteq G$ with $|A|\geq2$ and no unique sum has cardinality $\gg \log q(G)\,\log\log q(G)$ as $q(G)\to\infty$. The proof has two structural inputs. First, a maximum subset of $A$ whose distinct-element subset sums of size at most four are all different has cardinality $\gg\log p$. This follows from a short-coordinate lemma and a collision-lattice determinant argument. Second, we refine Bedert's density increment. Alternative representations are oriented toward an uncovered endpoint, coalesced by their translation, and separated into wide, exposed, and recurrent batches. A load-sensitive entropy lemma codes the recurrent translations using their actual final fibre multiplicities. The resulting global shift-set complexity is $\exp(O(K))$, where $K$ is the ratio of $|A|$ to the level-four additive dimension. This forces $K\gg\log\log p$, and the theorem follows. All headline statements and the structural implications used to derive them have also been checked in Lean 4 with explicit integer constants. As a secondary and logically independent result, we construct weakly ternary-balanced sets and obtain \[ m(p)\leq \frac{(\log p)^2}{2(\log 3)^2} +\left(\frac{2}{\log 3}+o(1)\right) \frac{(\log p)^2}{\log\log p}. \]
Problem
For an odd prime p, m(p) is the minimum size of a set A ⊆ Z/pZ with |A|≥2 having no unique sum. Determining its order of magnitude is Green's Problem 27. The best known lower bound (Bedert) was weaker than the desired log p log log p.
Approach
A maximum 4-dissociated subset of A is shown to have cardinality ≫ log p via a short-coordinate lemma and collision-lattice determinant argument. Bedert's density increment is refined by orienting alternative representations toward uncovered endpoints and coding recurrent translations with a load-sensitive entropy lemma. The result generalizes to finite Abelian groups parameterized by the least prime divisor. All headline statements and structural implications are checked in Lean 4 with explicit integer constants.
Results
The improved lower bound m(p) ≫ log p log log p is proven, strengthening Bedert's bound by an unbounded factor. The same estimate holds for finite Abelian groups G with least prime divisor q(G)>2 as q(G)→∞, with an explicit constant c_* = 1/(10 C_DR).