Read-back: Erdos142.erdos_139_szemeredi

The statement

The declaration takes two explicit arguments: a natural number $k$, and a proof $h_k$ of $1 < k$. Its conclusion is a statement about a function of a natural number $N$: it asserts that

$$\lim_{N \to \infty} \frac{r(k, N)}{N} = 0 ,$$

where the quotient is formed in $\mathbb{R}$ (both $r(k,N)$ and $N$ are natural numbers, each cast into $\mathbb{R}$), the limit is taken along the "eventually large" filter on $\mathbb{N}$, and convergence is convergence in the neighbourhood filter of $0$ in $\mathbb{R}$ with its usual topology. Unwound, the assertion is: for every $\varepsilon > 0$ there is an $N_0 \in \mathbb{N}$ such that for all natural numbers $N \ge N_0$ one has $\left| r(k,N)/N \right| < \varepsilon$. No rate of convergence, no explicit bound, and no uniformity in $k$ is claimed; $k$ is fixed before the limit is taken.

Two conventions are silently in play. First, division in $\mathbb{R}$ is a total function in this formalism, so at $N = 0$ the term $r(k,0)/0$ is defined and equals $0$ (Lean's convention $x/0 = 0$); since the limit is along $N \to \infty$, this value — and indeed any finite set of values — is irrelevant to the truth of the conclusion. Second, $N$ ranges over $\mathbb{N}$ only (it is forced to be a natural number by its use as the second argument of $r$), so this is a statement about a sequence, not about a real-variable limit.

Which $k$ the hypothesis admits

The hypothesis is $1 < k$ with $k : \mathbb{N}$. It therefore admits exactly $k \in \{2, 3, 4, 5, \dots\}$, and excludes $k = 0$ and $k = 1$. In particular the case $k = 2$ is within the scope of the theorem. The hypothesis is satisfiable (e.g. $k = 2$), so the statement is not vacuous.

Expansion of the imported definitions

The symbol $r(k,N)$ is not a standard notion; it is defined in the imported bundle, and its definition rests on a chain of three further definitions. All of them are stated for an arbitrary type $\alpha$ carrying an additive commutative monoid structure, and are used here at $\alpha = \mathbb{N}$. Throughout, lengths are elements of $\mathbb{N}^\infty = \mathbb{N} \cup \{\infty\}$ (the extended naturals), and a natural number $k$ appearing in a length slot is coerced into $\mathbb{N}^\infty$.

Arithmetic progression with given data. For a set $s \subseteq \alpha$, a length $l \in \mathbb{N}^\infty$, and elements $a, d \in \alpha$, the predicate "$s$ is an AP of length $l$ with first term $a$ and difference $d$" means the conjunction of two conditions:

$$\#_{\mathbb{N}^\infty}(s) = l \qquad\text{and}\qquad s = \{\, a + n\cdot d \;:\; n \in \mathbb{N},\ n < l \,\},$$

where $\#_{\mathbb{N}^\infty}(s)$ is the cardinality of $s$ measured in $\mathbb{N}^\infty$ (so it is $\infty$ when $s$ is infinite), $n\cdot d$ denotes the $n$-fold monoid sum $d + \cdots + d$, and the condition $n < l$ compares the coerced $n \in \mathbb{N}^\infty$ with $l$. Note that $s$ must equal that set exactly, not merely contain it, and that the cardinality clause is an independent requirement imposed on top of the set equality.

Arithmetic progression of a given length. "$s$ is an AP of length $l$" means: there exist $a, d \in \alpha$ such that the previous predicate holds for $s, l, a, d$. The first term and the difference are existentially quantified; $d = 0$ is not excluded a priori.

Progression-freeness. "$s$ is free of APs of length $l$" is defined as

$$\forall\, t \subseteq s,\quad \bigl(t \text{ is an AP of length } l\bigr) \;\Longrightarrow\; l \le 1 .$$

The conclusion of the implication is $l \le 1$ in $\mathbb{N}^\infty$ — not falsehood. So for a length $l$ with $l \le 1$ (i.e. $l = 0$ or $l = 1$) this predicate is satisfied by every set $s$ whatsoever; it acquires content only when $l \ge 2$. Under the hypothesis $1 < k$ of the theorem, the coerced length $l = k$ satisfies $\neg(k \le 1)$, and the predicate is therefore equivalent to: no subset $t$ of $s$ (subsets of every cardinality, finite or infinite, are quantified over) is an AP of length $k$ in the above sense.

Combining the expansions: for $k \ge 2$ and a set $S \subseteq \mathbb{N}$, "$S$ is free of APs of length $k$" says that there are no $a, d \in \mathbb{N}$ and no subset $t \subseteq S$ with

$$t = \{\, a,\; a + d,\; a + 2d,\; \dots,\; a + (k-1)d \,\} \qquad\text{and}\qquad \#_{\mathbb{N}^\infty}(t) = k .$$

Because the cardinality is required to be exactly $k \ge 2$, the case $d = 0$ cannot occur (it would make the displayed set the singleton $\{a\}$, of cardinality $1$); so the excluded configurations are precisely the genuine, non-degenerate $k$-term progressions with common difference $d \ge 1$, and each such $t$ is automatically finite with $k$ distinct members.

The counting function. For natural numbers $k$ and $N$,

$$r(k, N) \;=\; \sup \bigl\{\, |S| \;:\; S \text{ a finite subset of } \mathbb{N},\ S \subseteq \{1, 2, \dots, N\},\ S \text{ free of APs of length } k \,\bigr\},$$

where $|S|$ is the number of elements of $S$, the ambient interval is the integer interval from $1$ to $N$ inclusive, and the supremum is a supremum of a set of natural numbers. The set being supremized is non-empty (the empty set qualifies, contributing the value $0$; the bundle proves that the empty set is free of APs of every length) and bounded above by $N$, so this supremum is an honest maximum and there is no junk value here; the bundle separately proves $r(k,N) \le N$ for all $k, N$, and that every progression-free $S \subseteq \{1,\dots,N\}$ satisfies $|S| \le r(k,N)$. For $N = 0$ the interval $\{1,\dots,0\}$ is empty, so $r(k,0) = 0$.

Degenerate and boundary readings

• $N = 0$: $r(k,0)/0 = 0$ by the total-division convention; irrelevant to the limit.
• $k = 2$ is admitted by $1 < k$. With $k = 2$, every two-element subset $\{x, y\}$ of $S$ with $x < y$ is an AP of length $2$ (take $a = x$, $d = y - x$), so the freeness condition forces $|S| \le 1$ and hence $r(2, N) \le 1$ for all $N$.
• The freeness predicate ranges over all subsets $t \subseteq S$, not only those of size $k$; the size restriction comes from the cardinality clause inside the AP predicate.
• The bundle also defines an "elementary" pair of predicates — "$A$ has a $k$-term AP", meaning $\exists a, d \in \mathbb{N}$ with $0 < d$ and $a + i\,d \in A$ for every $i < k$, and its negation — but neither of these appears in the statement of this theorem; the theorem's $r$ is built solely from the cardinality-based definitions expanded above.
• Nothing in the statement asserts a lower bound on $r(k,N)$, positivity of $r(k,N)$, or monotonicity in $k$ or $N$.