A set with at most two representations of each difference is sparse

Let $T$ be a finite set of integers contained in an interval $[a,b]$, and suppose that for every non-zero $d$ there are at most two $n$ with $n, n+d \in T$. Then, writing $M = \#T$ and $N = b-a+1$ for the length of the interval,

Where this sits. This is the counting half of Theorem 3.6 (thm:power-support, Power-support sparsity) of the manuscript. There $T = S(z) \cap I$ for

and the hypothesis $\#\{n : n, n+d \in S(z)\} \le 2$ is supplied by the multiplier bound $\dim_{\bar{\mathbb{Q}}}\mathcal{M}_{z^{d}} \le 2$, itself a consequence of Roy's strong six exponentials theorem. Only the combinatorics is formalised here; the transcendence input is the hypothesis.

The manuscript's form of the conclusion. $M(M-1)/2 \le 2(N-1)$, equivalently

from which $S(z)$ has zero asymptotic density. The displayed integer inequality is the same statement with the square root cleared, which is what the Lean states.

Proof. Map each ordered pair of distinct elements of $T$ to its difference. The image lies in $[a-b, b-a] \setminus \{0\}$, a set of $2(N-1)$ integers, and each fibre has at most two elements by hypothesis, since the pair is determined by its first coordinate once the difference is fixed. Hence $M^{2} - M \le 2 \cdot 2(N-1)$.

Elementary double counting; possibly known, not checked against the literature.

Source. Carlo Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz (private manuscript, 15 August 2026). The mathematics is his; this node only records one step of it in Lean, and claims no novelty of its own.