def SumFree.IsSumFree (S : Finset ℤ) : Prop

A subset $S \subseteq \mathbb{Z}$ is sum-free if no two elements (possibly equal) sum to a third, i.e., $a + b \neq c$ for all $a, b, c \in S$.

theorem SumFree.middleThird_sumFree {p : ℕ} [NeZero p] (hp3 : p % 3 = 2) (hp2 : 2 < p) {a b : ZMod p} (ha1 : p / 3 < a.val) (ha2 : a.val ≤ 2 * p / 3) (hb1 : p / 3 < b.val) (hb2 : b.val ≤ 2 * p / 3) : ¬(p / 3 < (a + b).val ∧ (a + b).val ≤ 2 * p / 3)

Key arithmetic fact: when $p \equiv 2 \pmod{3}$ and $p > 2$, the "middle third" $(p/3, 2p/3]$ in $\mathbb{Z}/p\mathbb{Z}$ is sum-free, i.e., the sum of two elements of this interval lies outside it.

theorem SumFree.card_filter_mul_right {p : ℕ} [Fact (Nat.Prime p)] {a : ZMod p} (ha : a ≠ 0) (B : Finset (ZMod p)) : {t : ZMod p | t * a ∈ B}.card = B.card

For a nonzero $a \in \mathbb{Z}/p\mathbb{Z}$ (with $p$ prime) and any subset $B$, right-multiplication by $a$ is a bijection, so $|\{t : t a \in B\}| = |B|$.

theorem SumFree.card_filter_val_Ioc (p : ℕ) [NeZero p] (a b : ℕ) (hb : b < p) : {x : ZMod p | a < x.val ∧ x.val ≤ b}.card = b - a

The number of elements of $\mathbb{Z}/p\mathbb{Z}$ whose canonical representative lies in the integer interval $(a, b]$ equals $b - a$, provided $b < p$.

theorem SumFree.double_count {p : ℕ} [Fact (Nat.Prime p)] (A : Finset ℤ) (B : Finset (ZMod p)) (hA : ∀ a ∈ A, ↑a ≠ 0) : ∑ t : ZMod p, {a ∈ A | t * ↑a ∈ B}.card = A.card * B.card

Double-counting identity: summing over $t \in \mathbb{Z}/p\mathbb{Z}$ the number of $a \in A$ with $t \cdot a \in B$ equals $|A| \cdot |B|$, when every element of $A$ is nonzero mod $p$.

theorem SumFree.intCast_ne_zero_of_lt {p : ℕ} [Fact (Nat.Prime p)] {a : ℤ} (ha : a ≠ 0) (hap : a.natAbs < p) : ↑a ≠ 0

If a nonzero integer $a$ has $|a| < p$ (where $p$ is prime), then $a$ is nonzero modulo $p$.

theorem SumFree.erdos_sumFree (A : Finset ℤ) (hA : ∀ a ∈ A, a ≠ 0) : ∃ S ⊆ A, IsSumFree S ∧ A.card / 3 ≤ S.card

Erdős' sum-free subset theorem (Theorem 2.2.1, Erdős 1965). Every finite set $A$ of nonzero integers contains a sum-free subset $S \subseteq A$ with $|S| \geq |A|/3$. Proved by dilation modulo a prime $p \equiv 2 \pmod 3$ and averaging over the middle third of $\mathbb{Z}/p\mathbb{Z}$.