Read-back: Erdos142.green_tao_four

The literal assertion

The declaration asserts the existence of a single real number $c$ such that two things hold simultaneously: first, $c > 0$; and second, the inequality

$$r(4, N) \;\le\; \frac{N}{(\log N)^{c}}$$

holds eventually as $N$ ranges over the natural numbers with respect to the atTop filter — that is, there exists a threshold $N_0 \in \mathbb{N}$ such that the displayed inequality holds for every natural number $N \ge N_0$. Note the order of quantification: the constant $c$ is chosen first, once and for all, and only afterwards is the threshold $N_0$ allowed to be chosen (so $N_0$ may depend on $c$, but $c$ may not depend on $N$). No upper bound whatsoever is imposed on $c$; the only constraint on it is positivity. The inequality is non-strict ($\le$, not $<$), it is stated as an inequality between real numbers — the natural number $r(4,N)$ and the natural number $N$ are both cast into $\mathbb{R}$ — and it is a one-sided upper bound on $r(4,N)$: nothing is claimed in the other direction.

What $(\log N)^{c}$ means here

$\log$ is the real natural logarithm applied to the real cast of $N$, and because the exponent $c$ is a real number, the power $(\log N)^{c}$ is real exponentiation (Real.rpow), not iterated multiplication. For a base $x > 0$ this is $\exp(c \log x)$ as usual. Two total-function conventions are silently in force. (i) $\log 0 = 0$ and $\log 1 = 0$, so for $N \in \{0, 1\}$ the base is $0$; since $c > 0$, real exponentiation gives $0^{c} = 0$, and division by zero in this setting returns $0$, so for $N \in \{0,1\}$ the right-hand side would be $0$ and the inequality would read $r(4,N) \le 0$. (ii) The base $\log N$ is never negative for any natural $N$ (it is $0$ at $N = 0, 1$ and positive for $N \ge 2$), so the branch of real exponentiation used for negative bases never arises. Because the claim is only made eventually, the small values $N = 0, 1, 2$ (and any other finite initial segment) may simply be excluded by the choice of $N_0$; the statement makes no assertion about them. For $N \ge 3$ one has $\log N > 1$, so $(\log N)^{c} > 1$ and the right-hand side is genuinely smaller than $N$.

What $r(4,N)$ means (expanded from the bundle)

The symbol $r(k,N)$ is a custom definition in the accompanying bundle, not a standard library notion. It is defined as the supremum, taken inside $\mathbb{N}$, of the set of natural numbers

$$\bigl\{\, |S| \;:\; S \subseteq \{1, 2, \dots, N\} \text{ a finite set, and } S \text{ is "AP-of-length-}k\text{ free"} \,\bigr\},$$

where $\{1,\dots,N\}$ is the integer interval from $1$ to $N$ inclusive (so $0$ is not in the ground set, and the interval is empty when $N = 0$) and $|S|$ is the cardinality of $S$. Two accompanying lemmas in the bundle establish that this set of cardinalities is non-empty (the empty set qualifies) and bounded above by $N$, so the supremum is an honest maximum rather than the junk value $0$ that a supremum over $\mathbb{N}$ returns for an unbounded or empty set. In particular the bundle proves $r(k,N) \le N$ for all $k, N$, and proves that every progression-free $S \subseteq \{1,\dots,N\}$ satisfies $|S| \le r(k,N)$. In the theorem, $k$ is fixed to $4$.

What "AP-of-length-$k$ free" means (expanded from the bundle)

For a set $s$ and a length $l \in \mathbb{N} \cup \{\infty\}$, the bundle declares $s$ free of arithmetic progressions of length $l$ to mean:

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

Here "$t$ is an arithmetic progression of length $l$" means: there exist a first term $a$ and a common difference $d$ (both in the ambient additive commutative monoid, here $\mathbb{N}$) such that the extended-natural cardinality of $t$ equals $l$ and $t$ is exactly the set $\{\, a + n d \;:\; n \in \mathbb{N},\ n < l \,\}$. Both conditions are required: the set-equality and the cardinality equality.

Instantiating at $l = k = 4$ (the natural number $4$ cast into $\mathbb{N} \cup \{\infty\}$), the consequent $4 \le 1$ is false, so the definition unfolds to: no subset $t$ of $S$ is an arithmetic progression of length exactly $4$, i.e. there are no $a, d$ with $t = \{a, a+d, a+2d, a+3d\}$ and $|t| = 4$. The cardinality clause is what rules out degenerate progressions: taking $d = 0$ gives the singleton $\{a\}$, whose cardinality is $1 \ne 4$, so constant "progressions" do not count; conversely any $d \ge 1$ in $\mathbb{N}$ yields four distinct terms. Since $t$ ranges over all subsets of $S$ (including $S$ itself), this is equivalent to saying that $S$ contains four elements in arithmetic progression with positive common difference. Note also that this notion is defined with the consequent "$l \le 1$" precisely so that it becomes vacuous for lengths $0$ and $1$; at $l = 4$ that escape clause is inert.

Definitions present in the bundle but not used by the statement

The bundle also defines an elementary predicate HasAP ($\exists\, a, d$ with $d > 0$ and $a + i d \in A$ for all $i < k$) and its negation APFree. Neither of these appears anywhere in the statement of the theorem: $r$ is defined through the set-theoretic notion described above, not through APFree. The bundle further contains a lemma that the empty set is progression-free for every length.

Summary of quantifier structure

$$\exists\, c \in \mathbb{R},\quad c > 0 \;\wedge\; \exists\, N_0 \in \mathbb{N},\ \forall\, N \ge N_0,\quad r(4,N) \le \frac{N}{(\log N)^{c}} .$$

There are no other hypotheses, no typeclass side conditions on the theorem itself, and no free variables: the statement is closed.