# Power savings for intersective polynomial differences and prime arguments

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A power saving for square-difference-free sets](../../preprints/A-power-saving-for-square-difference-free-sets-September-24-2026/paper.pdf)

## Scope

The formalization proves a fixed power saving for sets with no nonzero square difference. There are absolute constants $c>0$ and $C$ such that every $A\subseteq\{1,\ldots,N\}$ satisfying $a-b\ne m^2$ for all $a,b\in A$ and integers $m\ge1$ has $|A|\le C N^{1-c}$. The bound is uniform for every integer $N\ge1$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Power saving for square-difference-free sets | [SquareDifference.lean](../ComparatorChallenges/SquareDifference.lean) |