Read-back: Erdos142.r_add_le

The statement

The declaration asserts, for every triple of natural numbers $k, M, N$ (all three are ordinary explicit universally quantified variables of type $\mathbb{N}$, with no side hypotheses whatsoever):

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

Here $M+N$ is ordinary addition in $\mathbb{N}$, and the right-hand side is ordinary addition in $\mathbb{N}$; both sides are natural numbers, so no subtraction or truncation is involved. That is the whole content: subadditivity of the function $r(k,\cdot)$ in its second argument, uniformly in $k$.

What $r$ means (expanded from the bundle)

$r$ is defined in the accompanying bundle as a noncomputable function $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ by

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

where:

• $\{1,\dots,N\}$ is the integer interval $[1, N]$ in $\mathbb{N}$ (so it is empty when $N = 0$);
• $|S|$ is the cardinality of the finite set $S$;
• the supremum is the supremum of a set of natural numbers, taken in the conditionally complete lattice $\mathbb{N}$ (it returns $0$ on an empty or unbounded index set; here the index set is always nonempty, since $S = \emptyset$ always qualifies, and always bounded above by $N$);
• $\mathrm{APFree}^{\ast}(S,k)$ is the bundle's predicate IsAPOfLengthFree applied to $S$ viewed as a subset of $\mathbb{N}$ and to $k$ coerced into $\mathbb{N} \cup \{\infty\}$.

What $\mathrm{APFree}^{\ast}(S,k)$ literally says (expanded)

Unfolding two further bundle definitions, $\mathrm{APFree}^{\ast}(S,k)$ states:

$$\forall\, t \subseteq S:\quad \Bigl(\exists\, a, d \in \mathbb{N}: \; \#t = k \;\wedge\; t = \{\, a + n\,d \;:\; n \in \mathbb{N},\; n < k \,\}\Bigr) \;\Longrightarrow\; k \le 1 .$$

Points to note about this expansion:

• $t$ ranges over arbitrary subsets of $\mathbb{N}$ contained in $S$ (not only finite ones, though every such $t$ is finite here since $S$ is).
• $\#t$ is the extended-natural cardinality of $t$, and the equation $\#t = k$ is an equality in $\mathbb{N}\cup\{\infty\}$; so the witnessing progression must have exactly $k$ elements.
• $n\,d$ is the $n$-fold sum $d + \dots + d$ in the additive monoid, which in $\mathbb{N}$ is the ordinary product $n \cdot d$.
• The common difference $d$ is not required to be nonzero, and the first term $a$ is not required to lie in $\{1,\dots,N\}$; the only constraint tying them to $S$ is $t \subseteq S$ together with the exact-cardinality condition. (For $k \ge 2$, the cardinality condition $\#t = k$ by itself forces $d \ne 0$, since $d = 0$ makes the displayed set a singleton.)
• The consequent $k \le 1$ does not mention $t$. So for $k \ge 2$ the predicate says exactly: no subset of $S$ is of the form $\{a, a+d, \dots, a+(k-1)d\}$ with exactly $k$ elements; and for $k \le 1$ the consequent is unconditionally true, so the predicate is vacuously satisfied by every set $S$.

Parameter values the statement silently includes

Because there are no hypotheses on $k$, $M$, $N$, the claim is asserted in particular for the following degenerate instances:

• $k = 0$ and $k = 1$. As noted, $\mathrm{APFree}^{\ast}(S,k)$ holds for every $S$ when $k \le 1$, so the defining supremum is over all subsets of $\{1,\dots,N\}$ and $r(k,N) = N$. The asserted inequality is then $M + N \le M + N$.
• $k = 2$. Every two-element subset $\{a, a+d\}$ of $S$ with $d \ne 0$ is a witness, so only sets of size $\le 1$ qualify.
• $M = 0$, $N = 0$, and $M = N = 0$. When the second argument is $0$, the interval $\{1,\dots,0\}$ is empty, the only admissible $S$ is $\emptyset$, and $r(k,0) = 0$. So the statement includes $r(k, N) \le r(k, 0) + r(k, N) = r(k,N)$ and $r(k,0) \le r(k,0)+r(k,0)$.
• There is no requirement that $M \le N$, that $M$ and $N$ be positive, or that $k \ge 3$.

Scope notes

The inequality is stated with $\le$, not $<$, and is a single unconditional implication-free inequality, not an equivalence. The intervals appearing on the two sides are $\{1,\dots,M+N\}$, $\{1,\dots,M\}$ and $\{1,\dots,N\}$ respectively — all three anchored at $1$; no translated interval such as $\{M+1,\dots,M+N\}$ occurs anywhere in the statement or in the definition of $r$.

The bundle also contains elementary predicates HasAP and APFree (existence of $a, d$ with $d > 0$ and $a + i\,d \in A$ for all $i < k$, and its negation). These are not referenced by $r$ or by this theorem; the progression-freeness used here is the IsAPOfLengthFree version expanded above.