Read-back: Erdos142.exists_ratio_tendsto_zero

What the statement asserts

The theorem is a single existence claim, with no free variables and no hypotheses:

There exists a natural number $k$ such that $k \ge 3$ and

$$\lim_{n \to \infty} \frac{r(k,n)}{r(k+1,n)} = 0 ,$$

where the quotient is formed in $\mathbb{R}$ after casting the two natural numbers $r(k,n)$ and $r(k+1,n)$ to reals, and the limit is the limit of the sequence indexed by $n \in \mathbb{N}$ along the "eventually large $n$" filter, converging to the real number $0$ in the standard topology of $\mathbb{R}$.

Unwinding the filter statement: for every $\varepsilon > 0$ there is an index $N$ such that for all natural $n \ge N$,

$$\left| \frac{r(k,n)}{r(k+1,n)} \right| < \varepsilon .$$

Note that the claim is existential in $k$, not universal: it suffices that one single value $k \ge 3$ has the stated limiting behaviour. Nothing is asserted about any other $k$, and no such $k$ is exhibited. The two quantities compared are indexed by consecutive parameters $k$ and $k+1$; since $k \ge 3$, the denominator's parameter satisfies $k+1 \ge 4$.

The quantity $r(k,N)$ (custom definition from the bundle)

$r$ is a function $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ defined as a supremum taken inside $\mathbb{N}$:

$$r(k,N) \;=\; \sup \Bigl\{\, |S| \;\Big|\; S \text{ a finite subset of } \mathbb{N},\; S \subseteq \{1, 2, \dots, N\},\; \mathrm{Free}(S, k) \,\Bigr\},$$

where $|S|$ is the cardinality of the finite set $S$, the interval $\{1,\dots,N\}$ is the integer interval from $1$ to $N$ inclusive (empty when $N = 0$), and $\mathrm{Free}(S,k)$ is the bundle's progression-freeness predicate described below, applied to $S$ viewed as a subset of $\mathbb{N}$ and to the length $k$ cast into the extended naturals $\mathbb{N} \cup \{\infty\}$.

The supremum is the one for natural numbers, which returns a junk value of $0$ for an empty or unbounded set of naturals. Here neither degeneracy is triggered by the definition itself: the empty set $S = \varnothing$ always belongs to the collection (it is contained in every interval and, by a lemma in the bundle, is progression-free for every length), so the collection contains $0$ and is nonempty; and every admissible $S$ satisfies $|S| \le N$, so the collection is bounded. Hence $r(k,N)$ is the largest cardinality of an admissible set. In particular $r(k,0) = 0$ for every $k$, since $\{1,\dots,0\} = \varnothing$.

The freeness predicate $\mathrm{Free}(s, l)$

For a set $s$ in an additive commutative monoid and a length $l \in \mathbb{N} \cup \{\infty\}$:

$$\mathrm{Free}(s,l) \;:\Longleftrightarrow\; \forall\, t \subseteq s,\quad \mathrm{IsAP}(t,l) \;\Rightarrow\; l \le 1 .$$

The conclusion $l \le 1$ does not depend on $t$; it is the fixed parameter $l$. Consequently, whenever $l \ge 2$ the predicate is equivalent to: no subset $t$ of $s$ satisfies $\mathrm{IsAP}(t,l)$. Whenever $l \le 1$ the predicate holds vacuously-by-conclusion for every set $s$. In the theorem the lengths used are $k \ge 3$ and $k+1 \ge 4$, so the second regime does not occur there.

Here $\mathrm{IsAP}(t,l)$ means: there exist $a$ and $d$ in the ambient monoid (for $r$, in $\mathbb{N}$, so $a, d \ge 0$) with both of the following:

1. the cardinality of $t$, measured in $\mathbb{N} \cup \{\infty\}$, equals $l$; and
2. $t$ is exactly equal to the set $\{\, a + n \cdot d \;:\; n \in \mathbb{N},\; n < l \,\}$ (comparison $n < l$ taken in the extended naturals; $n \cdot d$ is the $n$-fold sum of $d$, i.e. ordinary multiplication in $\mathbb{N}$).

So $t$ must be a set of the form $\{a,\, a+d,\, a+2d,\, \dots,\, a+(l-1)d\}$ when $l$ is finite (and $\{a, a+d, a+2d, \dots\}$ when $l = \infty$), and have exactly $l$ elements. The clause $|t| = l$ is what excludes the degenerate difference $d = 0$: for $d = 0$ the displayed set is the singleton $\{a\}$, whose cardinality is $1$, so condition 1 fails unless $l = 1$. There is no separate hypothesis $d > 0$ and no separate hypothesis $d \ne 0$; non-degeneracy is enforced solely through the cardinality clause. Likewise $t = \varnothing$ can satisfy $\mathrm{IsAP}$ only when $l = 0$.

Putting this together, for $k \ge 2$:

$$\mathrm{Free}(S,k) \;\Longleftrightarrow\; \text{no subset of } S \text{ is a } k\text{-element set of the exact form } \{a, a+d, \dots, a+(k-1)d\}.$$

Since $d$ ranges over $\mathbb{N}$, the progressions considered are non-decreasing; the extremes $a$ and $a + (k-1)d$ both lie in $S \subseteq \{1,\dots,N\}$, so in fact $a \ge 1$ for any nonempty admissible $S$.

Junk values and edge cases the statement silently includes

• Real division by zero. The expression $r(k,n) / r(k+1,n)$ uses real division, which in this setting is a total function returning $0$ when the denominator is $0$. So at any index $n$ where $r(k+1,n) = 0$ — for instance $n = 0$, where both numerator and denominator are $0$ — the term of the sequence is literally $0$, not undefined. The claim therefore never requires the denominator to be nonzero, and never asserts that it is.
• The limit is along $n \to \infty$ only. Any finite set of indices, including all degenerate small $n$, is irrelevant to the truth of the convergence claim.
• Casts. $r(k,n)$ and $r(k+1,n)$ are natural numbers; both are cast into $\mathbb{R}$ before dividing, so the quotient is a genuine real quotient, not natural-number (truncating) division. The quotient is always $\ge 0$, so the absolute value in the $\varepsilon$-characterisation is immaterial.
• No claim of positivity, monotonicity, or growth. The statement says nothing about $r(k,n)$ or $r(k+1,n)$ individually — not that either is positive, increasing in $n$, or increasing in $k$ — only about the limit of their ratio for one unspecified $k \ge 3$.
• Unused bundle material. The bundle also defines an elementary predicate "$A$ contains a $k$-term progression" (existence of $a$ and $d$ with $d > 0$ and $a + i d \in A$ for all $i < k$) and its negation, but the statement of this theorem does not refer to them; the notion of freeness actually used by $r$ is the set-equality-plus-cardinality one described above. The bundle's auxiliary lemmas (the empty set is free for every length; every free subset of $\{1,\dots,N\}$ has at most $r(k,N)$ elements; $r(k,N) \le N$) are likewise not part of what this theorem asserts.
• The proof is omitted. The declaration's body is a placeholder, so the file contains an assertion, not a verified derivation.