GPT 6 Astra Ultra attempt on Math-5387

Erdős Problem 42: reconstruction of the known general solution

1) Problem and source status

Write $[N]=\{1,\ldots,N\}$. A set is Sidon if an equality $a+b=c+d$ between its elements forces equality of the unordered pairs, with repeated summands allowed. The intended assertion is that, for every $M\geq1$ and all sufficiently large $N$, every nonempty Sidon set $A\subset[N]$ admits a Sidon set $B\subset[N]$ such that \[ |B|=M,\qquad (A-A)\cap(B-B)=\{0\}. \] The nonempty qualification matters: if $A=\varnothing$, the intersection is empty, and the appropriate formulation is containment in $\{0\}$.

The problem page checked on 23 September 2026 reports the general result as solved, following a proof generated by GPT 5.5 Pro prompted by Harjas Sandhu and subsequent discussion and formalization. The older local gpt_pro_5.4/42.tex and 42_v2.tex cover finite obstructions and the case $M=3$. This note gives a complete deduction of the general result from the precisely stated compact Cayley theorem below. That theorem is an external input; its substantial compactness proof is not reproduced here. This is an exposition of existing work, with no claim of a new solution or a newly checked Lean build.

2) The external theorem and the plan

For a function $h:\mathbb Z/p\mathbb Z\to\mathbb C$, use the normalized Fourier transform \[ \widehat h(r)=\frac1p\sum_{x\bmod p}h(x)e^{-2\pi i rx/p}. \] We use the following theorem in the compact Cayley route to Problem 42.

Compact Cayley theorem. For each integer $L\geq2$ and real $\eta>0$, there are $\varepsilon>0$ and $p_0$ such that, for every prime $p>p_0$, the following holds. If $T\subset\mathbb Z/p\mathbb Z$ satisfies \[ T=-T,\qquad 0\notin T,\qquad |T|\geq\eta p, \qquad \widehat{1_T}(r)\leq\varepsilon\quad(r\neq0), \] then there is a set $C$ of $L$ distinct residues with \[ c-c'\in T\quad\hbox{whenever }c,c'\in C,\ c\neq c'. \] The Fourier coefficients in this statement are real because $T=-T$. The hypothesis is an upper bound, not a bound on their absolute values. The exact theorem appears as Erdos42.CompactCayley.compact_cayley_clique in the public Lean source cited below. Its proof uses Fourier extraction, passage to a connected compact group, and a counting argument. Reading that statement and its downstream reduction does not constitute independently checking all of the formal development.

We will put the allowed differences in $T$. The Sidon condition will give the required Fourier upper bound. A translate of a sufficiently large clique has many points in an interval of length $N$, and an elementary greedy argument supplies a Sidon subset of those points.

3) Greedy extraction, with all collision types included

We first prove that every finite set $X\subset\mathbb Z$ with $|X|\geq2M^3$ contains a Sidon subset of size $M$.

Suppose a Sidon subset $S\subset X$ of size $k<M$ has already been chosen. An element $x\in X$ fails to extend it only if $x\in S$, or if a new nontrivial sum equality has one of the forms \[ x+a=b+c\quad(a,b,c\in S),\qquad 2x=a+b\quad(a,b\in S). \] Indeed, an equality with $x$ once on each side cancels to a trivial equality, while $2x=x+a$ forces $x=a$. The number of forbidden integers is therefore at most \[ k+k^3+\frac{k(k+1)}2<2M^3. \] Some point of $X$ remains available. Starting from the empty set and repeating this argument produces $M$ points. The midpoint equation $2x=a+b$ is necessary here because the Sidon convention permits equal summands.

4) The exact Fourier calculation

Fix a nonempty Sidon set $A\subset[N]$, and write $a=|A|$. Its positive differences are distinct, so \[ \frac{a(a-1)}2\leq N-1. \] By Bertrand's postulate choose a prime $p$ with $4N<p<8N$. All sums of two members of $A$ lie in an interval of length less than $p$; consequently $A$, reduced modulo $p$, is still Sidon. Put \[ D=A-A\pmod p,\qquad T=(\mathbb Z/p\mathbb Z)\setminus D. \] Then $T=-T$, $0\notin T$, and \[ |D|=a(a-1)+1\leq2N-1<p/2, \qquad |T|>p/2. \]

Let convolution mean the unnormalized sum $(f*g)(x)=\sum_y f(y)g(x-y)$ on the cyclic group. Every nonzero directed difference has exactly one representation, whereas zero has $a$ representations. Thus the following is an exact identity: \[ 1_D=1_A*1_{-A}-(a-1)1_{\{0\}}. \] For $r\neq0$, Fourier transformation gives \[ \widehat{1_T}(r) =\frac{a-1}{p}-p\left|\widehat{1_A}(r)\right|^2 \leq\frac{a-1}{p} \leq\frac{\sqrt{2N-2}}{4N}. \] The last bound tends to zero uniformly over every admissible $A$. No equidistribution assumption about $A$ is used.

5) Completing the general-$M$ argument

Fix $M\geq1$, put $R=2M^3$, and apply the compact Cayley theorem with $L=8R$ and $\eta=1/2$. Choose $N$ large enough that its prime $4N<p<8N$ exceeds $p_0$ and that $\sqrt{2N-2}/(4N)\leq\varepsilon$. These conditions depend only on $M$. The preceding calculation supplies a clique $C\subset\mathbb Z/p\mathbb Z$ of size $8R$ whose nonzero differences all avoid $D$.

Average over translates $t\in\mathbb Z/p\mathbb Z$: \[ \frac1p\sum_t |C\cap(t+[N])|=\frac{|C|N}{p}>R. \] Hence some $t$ has at least $R$ clique points in $t+[N]$. Define their integer lifts by \[ X=\{i\in[N]:t+i\pmod p\in C\}. \] Because $N<p$, these are distinct lifts, and $|X|\geq R$. For distinct $x,y\in X$, the residue of $x-y$ belongs to $T$. It follows in particular that the integer $x-y$ cannot belong to $A-A$. The greedy extraction lemma supplies a Sidon subset $B\subset X$ of size $M$. Its nonzero differences avoid $A-A$. Since both $A$ and $B$ are nonempty, zero belongs to both difference sets. This proves \[ (A-A)\cap(B-B)=\{0\} \] and completes the desired deduction for every fixed $M$.

6) Checks and scope of the conclusion

There are three distinctions worth making explicit. First, the large clique itself need not be Sidon; the greedy extraction is a separate step. Second, its vertices initially lie in a cyclic group; averaging over interval translates and then lifting them is what puts $B$ in the required integer interval. Third, a Sidon set can be maximal under inclusion without having maximum cardinality. Replacing an arbitrary $A$ by an inclusion-maximal set does not justify applying the Fourier uniformity theorem for cardinality-extremal Sidon sets. The proof here uses the uniform one-sided estimate instead.

The finite checks in verification/solved_42_43_checks.py check the exact modular difference identity and density estimate for every nonempty Sidon subset of $[N]$, $1\leq N\leq12$. They are consistency checks for the elementary reduction. They do not prove the compact Cayley theorem or certify a threshold for arbitrary $M$. The present argument is qualitative and makes no explicit bound on $N_0(M)$.

Outcome: SOLVED, as a reconstruction using a cited external theorem. The deduction after the compact Cayley theorem has no remaining gap; that theorem is the stated mathematical dependency of this note.

7) Sources and attribution

• T. F. Bloom, problem page and discussion for Problem 42, https://www.erdosproblems.com/42 and https://www.erdosproblems.com/forum/discuss/42, checked 23 September 2026. The discussion attributes the general solution to GPT 5.5 Pro prompted by Harjas Sandhu, with subsequent exposition and analysis by the contributors named there.
• Public compact Cayley formal development, https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P42/CompactCayley/Proof.lean, in particular compact_cayley_clique and theorem_1_1_from_compact_cayley, source read 23 September 2026. The source declares only Lean/Mathlib core axioms for these exposed theorems. No local type-checking is claimed here.

The estimate measures coverage of the intended nonempty-$A$ problem by the reconstruction, with the explicitly cited theorem accepted. It does not measure novelty or an independent formal verification.

8) COMPLETION ESTIMATE

COMPLETION: 100%