Read-back: Erdos142.behrend_lower_bound

The statement

The declaration asserts a single claim, universally quantified over every natural number $N$, with no hypotheses whatsoever (in particular $N = 0$ and $N = 1$ are included):

$$N \cdot \exp\!\left(-4\,\sqrt{\log N}\right) \;\le\; r(3, N).$$

Here $N$ on the left is the image of the natural number $N$ under the canonical embedding $\mathbb{N} \hookrightarrow \mathbb{R}$, $\log$ is the real natural logarithm, $\sqrt{\cdot}$ is the real square root, $\exp$ is the real exponential, and the right-hand side is the natural number $r(3,N)$ (defined below) likewise cast into $\mathbb{R}$. The inequality is non-strict ($\le$), and it is a lower bound on $r(3,N)$. The exponent is the product of the real constant $-4$ with $\sqrt{\log N}$.

What $r(k, N)$ means in this file

The quantity $r(k,N)$ is not a Mathlib notion; it is defined in the imported bundle as a natural number given by a supremum of a set of natural numbers:

$$r(k, N) \;=\; \sup\Bigl\{\, |S| \;\Bigm|\; S \subseteq \{1, 2, \ldots, N\},\ \ S \text{ is } \mathrm{APFree}_k \,\Bigr\},$$

where $S$ ranges over finite subsets of $\mathbb{N}$, $|S|$ is its cardinality, and $\{1,\dots,N\}$ is the integer interval from $1$ to $N$ inclusive (which is empty when $N = 0$). The supremum is taken in $\mathbb{N}$; the defining set is always non-empty (it contains $|\emptyset| = 0$) and is bounded above by $N$, so this is a genuine maximum. The bundle also records, as separate already-proved facts, that the empty set is progression-free for every length, that any progression-free $S \subseteq \{1,\dots,N\}$ satisfies $|S| \le r(k,N)$, and that $r(k,N) \le N$ for all $k, N$. The theorem instantiates $k = 3$.

What "progression-free" means in this file

The predicate applied to $S$ above is, unfolded completely, the following. Working in an arbitrary additive commutative monoid $\alpha$ (instantiated here at $\alpha = \mathbb{N}$, with $S$ viewed as a set of naturals), and with a length parameter $l$ living in the extended naturals $\mathbb{N} \cup \{\infty\}$ (here $l = 3$, the natural number $3$ coerced into the extended naturals):

• A set $t \subseteq \alpha$ is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when both

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

where $\#t$ is the extended-natural cardinality of $t$ and $n \cdot d$ is the $n$-fold monoid multiple of $d$ (ordinary multiplication when $\alpha = \mathbb{N}$).

• A set $t$ is an arithmetic progression of length $l$ when such $a$ and $d$ exist.
• A set $s$ is progression-free of length $l$ when

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

Because the theorem fixes $l = 3$, the conclusion $l \le 1$ of that implication is false, so for $l = 3$ the predicate is equivalent to: no subset $t$ of $s$ is an arithmetic progression of length $3$, i.e. there are no $a, d$ with $\{a, a+d, a+2d\} \subseteq s$ and $\#\{a, a+d, a+2d\} = 3$. The cardinality clause forces the three terms to be distinct, hence $d \ne 0$; a constant "progression" with $d = 0$ has cardinality $1$ and is therefore not excluded. Note the second clause demands set equality $t = \{a, a+d, a+2d\}$, not merely containment, so $t$ is exactly the three-term progression.

The bundle additionally defines two elementary predicates — "$A$ contains a $k$-term progression" ($\exists\, a, d$ with $d > 0$ and $a + i d \in A$ for all $i < k$) and its negation — but neither of these is used by $r$ or by the theorem; the theorem's notion of progression-freeness is exclusively the set-and-cardinality one spelled out above.

Degenerate and edge cases the quantifier silently includes

• $N = 0$. The cast of $0$ into $\mathbb{R}$ is $0$, so by Mathlib's convention $\log 0 = 0$ (the logarithm is a total function taking the junk value $0$ at $0$ and at all non-positive reals), hence $\sqrt{\log 0} = \sqrt{0} = 0$ and $\exp(0) = 1$. The left-hand side is therefore $0 \cdot 1 = 0$. Meanwhile $\{1,\dots,0\}$ is empty, so the only admissible $S$ is $\emptyset$ and $r(3,0) = 0$. The claim in this case reads $0 \le 0$.
• $N = 1$. Again $\log 1 = 0$, $\sqrt{0} = 0$, $\exp(0) = 1$, so the left-hand side is exactly $1$, and the claim reads $1 \le r(3,1)$.
• Square root at small arguments. Mathlib's Real.sqrt is total and returns $0$ on every non-positive input. Since $\log N \ge 0$ for every natural $N \ge 1$ and $\log 0 = 0$ by the convention above, the argument of the square root is never negative for any $N$ in this statement, so the $\sqrt{\cdot}$ junk-value branch is never reached; only the $\log$ convention at $N = 0$ is load-bearing.
• Sign of the exponent. For $N \ge 2$ the exponent $-4\sqrt{\log N}$ is strictly negative, so the exponential factor lies strictly between $0$ and $1$ and the left-hand side is strictly less than $N$; the claim is thus weaker than $N \le r(3,N)$ for those $N$.
• No hypothesis restricts $N$ to be large, positive, or of any particular form, and no hypothesis in the statement is vacuous or unsatisfiable — the statement is a bare universally quantified inequality.