Read-back: Erdos142.kelley_meka

The literal assertion

The theorem asserts the existence of a single real constant $c$ such that

$$c > 0 \qquad\text{and}\qquad r(3, N) \;\le\; N \cdot \exp\!\big(-c \cdot (\log N)^{1/12}\big) \quad\text{for all sufficiently large } N \in \mathbb{N}.$$

Here $r(3,N)$ is a natural number that is cast into $\mathbb{R}$ before the comparison, $N$ on the right-hand side is likewise the real cast of the natural number $N$, $\log$ is the natural logarithm on $\mathbb{R}$, and $\exp$ is the real exponential.

Quantifier order matters and is exactly this: first a real $c$ is chosen, then positivity of $c$ is asserted, and only then the "eventually" claim is made. The filter used is the "at infinity" filter on $\mathbb{N}$, so "eventually" unfolds to: there exists a threshold $N_0 \in \mathbb{N}$ such that the displayed inequality holds for every natural $N \ge N_0$. Because the threshold is introduced after $c$, $N_0$ is allowed to depend on $c$. Nothing constrains $c$ from above, nothing constrains $N_0$, and no lower bound on $r(3,N)$ is claimed. The inequality is non-strict ($\le$).

The statement is made only for the value $3$ in the first argument of $r$; nothing is asserted about $r(k,N)$ for any other $k$.

What $r(3,N)$ means in this bundle

$r$ is defined in the imported bundle, not taken from any standard library, as

$$r(k,N) \;=\; \sup\;\Big\{\, |S| \;:\; S \subseteq \{1,2,\dots,N\} \text{ a finite set, } S \text{ is "AP-of-length-}k\text{ free"} \,\Big\},$$

where $\{1,\dots,N\}$ is the integer interval from $1$ to $N$ inclusive, $|S|$ is the cardinality of the finite set $S$, and the supremum is the supremum in $\mathbb{N}$. The index set of the supremum always contains $0$ (take $S = \emptyset$) and is bounded above by $N$, so the supremum is an honest maximum; in particular the degenerate supremum convention (value $0$ for an empty or unbounded index set) is never triggered. Two auxiliary lemmas in the bundle, both fully proved, record exactly this: every progression-free $S \subseteq \{1,\dots,N\}$ satisfies $|S| \le r(k,N)$, and $r(k,N) \le N$ for all $k,N$.

What "AP-of-length-$k$ free" means in this bundle

The freeness predicate applied to the set $S$ (viewed as a subset of $\mathbb{N}$) with length parameter $3$ is defined as:

for every subset $t \subseteq S$, if $t$ is an arithmetic progression of length $3$, then $3 \le 1$.

Since $3 \le 1$ is false, this is equivalent to: no subset of $S$ is an arithmetic progression of length $3$.

"$t$ is an arithmetic progression of length $l$" is in turn defined as: there exist $a, d$ (elements of the ambient additive commutative monoid, here $a, d \in \mathbb{N}$) such that

1. the cardinality of $t$, measured in $\mathbb{N} \cup \{\infty\}$, equals $l$; and
2. $t$ is exactly the set $\{\, a + n\cdot d \;:\; n \in \mathbb{N},\ n < l \,\}$.

For $l = 3$ this says $t = \{a,\ a+d,\ a+2d\}$ and $|t| = 3$. The cardinality clause is a genuine extra requirement: it forces $a$, $a+d$, $a+2d$ to be three distinct elements, which over $\mathbb{N}$ rules out $d = 0$. So the common difference is never zero in the progressions that are forbidden, even though the definition itself never mentions $d \ne 0$; and the definition requires $t$ to equal the three-element progression, not merely to contain it.

Note that this is the set-theoretic notion of a progression: an unordered three-element subset $\{a, a+d, a+2d\} \subseteq \mathbb{N}$. Also note that the length parameter of the freeness predicate has type $\mathbb{N} \cup \{\infty\}$, and the natural number $3$ appearing in $r(3,N)$ is coerced into it.

The real-exponent power

The expression $(\log N)^{1/12}$ uses the exponent $1/12$ as a real number, so the power is the real-exponent power (rpow), not iterated multiplication. For a base $x > 0$ this is the ordinary $\exp\big(\tfrac{1}{12}\log x\big)$, i.e. the real twelfth root. Its total-function conventions matter only at small $N$: for $N = 0$ and $N = 1$ the logarithm is $0$ (with $\log 0 = 0$ by the library's convention), and $0^{1/12} = 0$ since the exponent is nonzero, so the bound degenerates to $r(3,N) \le N$ there. For every $N \ge 2$ the base $\log N$ is strictly positive, so the negative-base branch of the real power (where $x^y = |x|^y \cos(\pi y)$ for $x < 0$) is never reached at any $N \ge 1$. Because the claim is only made eventually, none of these small values is actually asserted about.

Degenerate and edge cases folded into the statement

• $r(3,0) = 0$, since $\{1,\dots,0\}$ is empty; $r(3,N)$ is always at least $0$ and at most $N$, so the asserted inequality is a statement strictly stronger than the trivial bound $r(3,N) \le N$ exactly because the exponential factor $\exp(-c(\log N)^{1/12})$ is $< 1$ for $N \ge 2$ and $c > 0$.
• The freeness hypothesis inside the definition of $r$ is satisfiable (the empty set is progression-free, and this is proved in the bundle), so the supremum's index set is nonempty; the theorem is not vacuous on that account.
• The theorem carries no hypotheses of its own: there are no variables bound outside it and no typeclass assumptions beyond those built into $\mathbb{R}$ and $\mathbb{N}$. The bundle's definitions are stated for a general additive commutative monoid $\alpha$, but the theorem instantiates them at $\alpha = \mathbb{N}$ only.

Items present in the bundle but not used by this statement

The bundle also defines an "elementary" pair of predicates: $\mathrm{HasAP}(k, A)$, saying there exist $a$ and $d$ with $d > 0$ such that $a + i\,d \in A$ for every $i < k$ (a containment condition on an indexed progression, with no distinctness or exact-equality requirement), and $\mathrm{APFree}(k,A)$, its negation. Neither of these appears in the definition of $r$ nor in the theorem; the theorem's notion of progression-freeness is solely the set-equality-plus-cardinality one described above.

Proof status

The proof of the theorem is left unfilled in the file (sorry); only the auxiliary bundle lemmas about the empty set, the lower bound $|S| \le r(k,N)$, and the upper bound $r(k,N) \le N$ carry complete proofs.