Read-back — Erdos142Basic.lean

The whole file lives in a namespace Erdos142 and imports all of Mathlib. Two of the declarations below are stated for an arbitrary ambient type $\alpha$ carrying the structure of an additive commutative monoid (so $\alpha$ has an addition that is associative and commutative, and a neutral element $0$; there is no subtraction, no order, and no cancellation available). The remaining declarations are stated concretely for the natural numbers $\mathbb{N}$.

Throughout, $\mathbb{N}_\infty$ denotes the extended naturals $\mathbb{N} \cup \{\infty\}$ (ℕ∞), with $\infty$ (written $\top$) as the largest element, and $\#s$ denotes the $\mathbb{N}_\infty$-valued cardinality of a set $s$ (ENat.card), which equals the ordinary number of elements when $s$ is finite and equals $\infty$ when $s$ is infinite. For $n \in \mathbb{N}$ and $d \in \alpha$, $n \cdot d$ denotes the monoid multiple $d + \dots + d$ ($n$ summands), with $0 \cdot d = 0$.

---

1. IsAPOfLengthWith (definition)

For an additive commutative monoid $\alpha$, a set $s \subseteq \alpha$, an extended natural number $l \in \mathbb{N}_\infty$, and two elements $a, d \in \alpha$, the proposition $\mathrm{IsAPOfLengthWith}(s, l, a, d)$ is defined to be the conjunction of two conditions:

$$\#s = l \qquad\text{and}\qquad s = \{\, a + n\cdot d \;:\; n \in \mathbb{N},\ n < l \,\}.$$

Here the comparison $n < l$ is taken in $\mathbb{N}_\infty$ after coercing the natural number $n$; the second condition is a set equality (both inclusions), where the right-hand side is the set of all elements expressible as $a + n \cdot d$ for some natural number $n$ strictly below $l$.

Points that this definition silently includes:

• Nothing forbids $d = 0$. If $d = 0$ then the right-hand set is $\{a\}$ when $l \ge 1$ and $\emptyset$ when $l = 0$; the first conjunct $\#s = l$ then forces $l = 1$ (resp. $l = 0$), so the two conjuncts together can only be met at $l \le 1$ in that case.
• $l = 0$: the right-hand set is empty (no natural number is $< 0$) and $\#s = 0$, so the definition holds exactly when $s = \emptyset$, and it then holds for every choice of $a$ and $d$.
• $l = 1$: the right-hand set is $\{a + 0\cdot d\} = \{a\}$ and $\#s = 1$, so the definition holds exactly when $s = \{a\}$, again for every choice of $d$.
• $l = \infty$: every natural number satisfies $n < \infty$, so the right-hand set is the full forward orbit $\{a + n\cdot d : n \in \mathbb{N}\}$, and $\#s = \infty$ requires $s$ to be infinite.
• There is no injectivity hypothesis on $n \mapsto a + n\cdot d$; the only thing that constrains repetitions is the cardinality equation $\#s = l$, which requires the displayed set to have exactly $l$ elements. In particular the condition is an exact cardinality, not an inequality.
• $a$ itself is always a member of $s$ whenever $l \ge 1$ (take $n = 0$).

2. IsAPOfLength (definition)

For an additive commutative monoid $\alpha$, a set $s \subseteq \alpha$ and $l \in \mathbb{N}_\infty$, the proposition $\mathrm{IsAPOfLength}(s, l)$ says that there exist $a \in \alpha$ and $d \in \alpha$ such that $\mathrm{IsAPOfLengthWith}(s, l, a, d)$ holds, i.e. such that

$$\#s = l \qquad\text{and}\qquad s = \{\, a + n\cdot d : n \in \mathbb{N},\ n < l \,\}.$$

Both $a$ and $d$ are existentially quantified over all of $\alpha$; in particular $d = 0$ is an allowed witness. By the previous item, $\mathrm{IsAPOfLength}(s, 0)$ holds precisely when $s = \emptyset$, and $\mathrm{IsAPOfLength}(s, 1)$ holds precisely when $s$ is a singleton (both because $\alpha$, being a monoid, is nonempty and supplies witnesses $a, d$).

3. IsAPOfLengthFree (definition)

For an additive commutative monoid $\alpha$, a set $s \subseteq \alpha$ and $l \in \mathbb{N}_\infty$, the proposition $\mathrm{IsAPOfLengthFree}(s, l)$ is defined as:

$$\forall\, t \subseteq s,\quad \mathrm{IsAPOfLength}(t, l) \;\longrightarrow\; l \le 1 .$$

The quantifier ranges over all subsets $t$ of $s$ (including $t = \emptyset$ and $t = s$). Note that the conclusion of the implication is $l \le 1$, a statement about $l$ alone that does not mention $t$ or $s$. Consequently the definition is logically equivalent to

$$l \le 1 \quad\text{or}\quad \bigl(\text{no subset } t \subseteq s \text{ satisfies } \mathrm{IsAPOfLength}(t,l)\bigr).$$

Degenerate readings this entails:

• For $l = 0$ and for $l = 1$ the conclusion $l \le 1$ is true outright, so $\mathrm{IsAPOfLengthFree}(s, l)$ holds vacuously for every set $s$ whatsoever, including $s = \alpha$.
• For $l \ge 2$ (including $l = \infty$) the definition says: no subset $t \subseteq s$ satisfies $\#t = l$ together with $t = \{a + n\cdot d : n < l\}$ for some $a, d \in \alpha$. Because $\#t = l \ge 2$ cannot hold when $d = 0$ (that set is a singleton), the excluded configurations are automatically ones with $d \ne 0$; but this is a consequence of the cardinality equation, not a separately stated hypothesis.
• The excluded $t$ must be exactly equal to the progression set $\{a + n\cdot d : n < l\}$, not merely contain it.

4. r (noncomputable definition)

For natural numbers $k$ and $N$, the natural number $r(k, N)$ is defined as the supremum, taken in $\mathbb{N}$, of the set of cardinalities

$$\bigl\{\, |S| \;:\; S \text{ a finite set of naturals},\ S \subseteq \{1, 2, \dots, N\},\ \mathrm{IsAPOfLengthFree}(S, k) \,\bigr\} \subseteq \mathbb{N},$$

where $S$ ranges over finite subsets of $\mathbb{N}$, the containment is in the integer interval $\{m \in \mathbb{N} : 1 \le m \le N\}$ (which is empty when $N = 0$), $|S|$ is the number of elements of $S$, and the freeness condition is $\mathrm{IsAPOfLengthFree}$ of item 3 applied to $S$ viewed as a set of naturals, at the length $k$ coerced into $\mathbb{N}_\infty$ (so the length is always a genuine natural number here, never $\infty$).

Conventions that this definition carries:

• The supremum is the $\mathbb{N}$-valued supremum. On $\mathbb{N}$ this operation returns the junk value $0$ whenever the set has no greatest element — that is, when the set is empty, and also when it is nonempty but unbounded above. It returns the actual maximum only when the set is nonempty and bounded.
• By item 3, when $k = 0$ or $k = 1$ the freeness condition is satisfied by every $S$, so the set being maximised is the set of all cardinalities of subsets of $\{1,\dots,N\}$.
• The empty set $S = \emptyset$ always satisfies both side conditions (see item 7), so $0$ always belongs to the set; and every $S$ in the set has $|S| \le N$. Hence in this particular definition the supremum is an honest maximum and no junk value is triggered.
• No lower bound $k \ge 3$, and no restriction such as $d \ne 0$, appears anywhere in the definition.

5. HasAP (definition)

For a natural number $k$ and a finite set of natural numbers $A$, the proposition $\mathrm{HasAP}(k, A)$ says:

$$\exists\, a \in \mathbb{N},\ \exists\, d \in \mathbb{N},\quad d > 0 \ \text{ and } \ \forall i \in \mathbb{N} \text{ with } i < k,\ \ a + i\,d \in A .$$

Here $a$ is allowed to be $0$, $d$ is required to be strictly positive, and $i\,d$ is ordinary multiplication of naturals. Edge cases:

• For $k = 0$ the inner universal statement is vacuous, so $\mathrm{HasAP}(0, A)$ holds for every $A$, including $A = \emptyset$ (witnesses $a = 0$, $d = 1$).
• For $k = 1$ the statement reduces to $\exists a,\ a \in A$, i.e. $\mathrm{HasAP}(1, A)$ holds exactly when $A \ne \emptyset$.
• Since $d > 0$, the $k$ listed terms $a, a+d, \dots, a+(k-1)d$ are pairwise distinct naturals.

6. APFree (definition)

For a natural number $k$ and a finite set of natural numbers $A$, $\mathrm{APFree}(k, A)$ is defined to be the negation $\neg\,\mathrm{HasAP}(k, A)$, i.e. there are no $a \in \mathbb{N}$ and $d \in \mathbb{N}$ with $d > 0$ such that $a + i\,d \in A$ for all $i < k$. By the previous item, $\mathrm{APFree}(0, A)$ is false for every $A$, and $\mathrm{APFree}(1, A)$ holds exactly when $A = \emptyset$.

These two elementary predicates $\mathrm{HasAP}$ and $\mathrm{APFree}$ are not referred to by any other declaration in this file; in particular no declaration here relates them to $\mathrm{IsAPOfLengthFree}$ or to $r$.

7. isAPOfLengthFree_empty (theorem)

For every additive commutative monoid $\alpha$ (implicit type argument, with its AddCommMonoid instance) and every natural number $k$, the empty subset of $\alpha$ satisfies

$$\mathrm{IsAPOfLengthFree}(\emptyset,\ k),$$

where $k$ is coerced into $\mathbb{N}_\infty$. Unfolded, the assertion is: for every set $t \subseteq \emptyset$, if there exist $a, d \in \alpha$ with $\#t = k$ and $t = \{a + n\cdot d : n < k\}$, then $k \le 1$. The only such $t$ is $\emptyset$, whose cardinality is $0$, so the hypothesis forces $k = 0$ and hence $k \le 1$. The statement is asserted only for lengths that are natural numbers; the case $k = \infty$ is not covered by this declaration.

8. le_r (theorem)

Let $S$ be a finite set of natural numbers and let $k$ and $N$ be natural numbers (all three are implicit arguments). Assume:

1. $S \subseteq \{1, 2, \dots, N\}$; and
2. $\mathrm{IsAPOfLengthFree}(S, k)$ — that is, for every set $t \subseteq S$, if $t$ is an arithmetic progression of length exactly $k$ in the sense of item 2, then $k \le 1$.

Then

$$|S| \;\le\; r(k, N),$$

with $r$ as defined in item 4 (the $\mathbb{N}$-valued supremum of the cardinalities of all progression-free subsets of $\{1,\dots,N\}$). Note that for $k = 0$ and $k = 1$ hypothesis 2 is automatically satisfied by every $S$, so in those cases the theorem asserts $|S| \le r(k,N)$ for every $S \subseteq \{1,\dots,N\}$.

9. r_le (theorem)

For all natural numbers $k$ and $N$,

$$r(k, N) \;\le\; N .$$

This is asserted for every $k$ without exception, including $k = 0$ and $k = 1$, and for every $N$, including $N = 0$ (where $\{1,\dots,N\}$ is empty).