Read-back: Erdos142.r_mono_length

The statement

For all natural numbers $k$, $l$, $N$, if

• $2 \le k$, and
• $k \le l$,

then

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

All three of $k$, $l$, $N$ are ordinary natural numbers (so $l \ge 2$ follows from the two hypotheses, and $N$ is unconstrained, including $N = 0$). There are no other hypotheses: no typeclass assumptions beyond those built into $\mathbb{N}$, no positivity or size condition on $N$, and no relation between $N$ and $k$ or $l$. The quantity $N$ is the same on both sides of the inequality; only the first argument changes.

What $r(k, N)$ denotes (expanded from the bundle)

The bundle defines, for natural numbers $k$ and $N$,

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

where the supremum is the supremum of a set of natural numbers taken in $\mathbb{N}$ (with the convention that the supremum of an empty or unbounded set of naturals is $0$), $S$ ranges over finite subsets of $\mathbb{N}$, $\{1,\dots,N\}$ is the integer interval from $1$ to $N$ inclusive (empty when $N = 0$), $|S|$ is the number of elements of $S$, and $\mathrm{APFree}^{\ast}$ is the bundle's predicate IsAPOfLengthFree applied to $S$ viewed as a set of naturals and to $k$ coerced into $\mathbb{N} \cup \{\infty\}$.

Unwinding that predicate through the bundle's chain of definitions: for a set $s \subseteq \mathbb{N}$ and a length $\lambda \in \mathbb{N} \cup \{\infty\}$,

• $s$ is an arithmetic progression of length $\lambda$ with first term $a$ and difference $d$ (IsAPOfLengthWith) means both

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

where $\#\,s$ is the cardinality of $s$ as an element of $\mathbb{N} \cup \{\infty\}$ ($\infty$ if $s$ is infinite), and $n\,d$ is $d$ added to itself $n$ times (ordinary multiplication in $\mathbb{N}$).

• $s$ is an arithmetic progression of length $\lambda$ (IsAPOfLength) means there exist $a, d \in \mathbb{N}$ making the above hold. Note $d$ is only required to be a natural number; it is not required to be nonzero, and $a$ is not required to be nonzero.
• $s$ is free of arithmetic progressions of length $\lambda$ (IsAPOfLengthFree) means

$$\forall\, t \subseteq s,\quad \bigl(t \text{ is an arithmetic progression of length } \lambda\bigr) \;\longrightarrow\; \lambda \le 1 .$$

Two features of this last definition are worth stating explicitly, because they are what the code literally says. First, the conclusion $\lambda \le 1$ does not mention $t$: the predicate is therefore equivalent to "if some subset of $s$ is an arithmetic progression of length $\lambda$, then $\lambda \le 1$". Consequently, for $\lambda \le 1$ the predicate holds vacuously for every set $s$, and for $\lambda \ge 2$ it says exactly that no subset of $s$ is an arithmetic progression of length $\lambda$. Since the theorem assumes $2 \le k \le l$, both occurrences of the predicate in this theorem fall in the second regime. Second, the subsets $t$ range over arbitrary subsets of $s$ as a set of naturals, and $t$ must be equal to the progression $\{a + n d : n < \lambda\}$, not merely contain it.

Putting these together, for $k \ge 2$ the condition on $S$ in the definition of $r(k, N)$ reads: there do not exist $a, d \in \mathbb{N}$ such that the set $\{a, a+d, a+2d, \dots, a+(k-1)d\}$ has exactly $k$ elements and is contained in $S$. The cardinality clause $\#\,t = k$ is what rules out the degenerate difference: if $d = 0$ the listed set is $\{a\}$, whose cardinality is $1 \ne k$ for $k \ge 2$, so such a $t$ is never a witness. Since $\mathbb{N}$ has no negative elements, $d \ge 1$ in every non-degenerate case, so the progressions being excluded are strictly increasing $k$-term progressions.

What the supremum evaluates to

The set of cardinalities being maximised always contains $0$ (take $S = \emptyset$, which is a subset of $\{1,\dots,N\}$ and is progression-free for every length, per the bundle's isAPOfLengthFree_empty), and it is bounded above by $N$ (per the bundle's r_le). Hence for every $k$ and $N$ the supremum is attained: $r(k, N)$ is the largest cardinality of a subset of $\{1,\dots,N\}$ containing no $k$-term arithmetic progression with $k$ distinct terms, and $0 \le r(k, N) \le N$.

Edge cases silently included

• $N = 0$: the interval $\{1,\dots,0\}$ is empty, the only admissible $S$ is $\emptyset$, and the assertion becomes $0 \le 0$.
• $k = l$: the hypotheses are satisfiable and the conclusion is the trivial $r(k,N) \le r(k,N)$.
• $k = 2$ (the smallest allowed value): a $2$-term progression with two distinct terms is any pair of distinct elements, so $r(2,N)$ is the largest size of a subset of $\{1,\dots,N\}$ with no two distinct elements, i.e. $r(2,N) = 1$ for $N \ge 1$.
• $l$ may be arbitrarily large relative to $N$; nothing forces $l \le N$.
• The hypotheses are jointly satisfiable (e.g. $k = l = 2$), so the statement is not vacuous.

What the statement does not cover

• It says nothing for $k \le 1$: the hypothesis $2 \le k$ excludes $k = 0$ and $k = 1$, the two cases in which the progression-freeness predicate degenerates to "always true" and $r(k,N)$ would equal $N$.
• It says nothing about infinite length: $k$ and $l$ are natural numbers, so the value $\infty$ of the length parameter $\lambda \in \mathbb{N} \cup \{\infty\}$ permitted by the bundle's definitions never occurs here.
• It asserts a non-strict inequality only; it does not claim $r(k,N) < r(l,N)$ when $k < l$, nor any quantitative gap, nor any growth or asymptotic behaviour in $N$.
• It says nothing about monotonicity or any other behaviour in $N$, and nothing about the actual size of $r(k,N)$ beyond what the definition entails.
• The bundle also defines an elementary predicate $\mathrm{HasAP}(k, A)$ ("there exist $a$ and $d > 0$ with $a + i d \in A$ for all $i < k$") and its negation $\mathrm{APFree}(k,A)$. Neither of these appears in the definition of $r$ or in this theorem; $r$ is defined solely through the IsAPOfLengthFree chain expanded above.

Proof status

The declaration is stated with its proof left as sorry; the file asserts the statement without establishing it.