Read-back: Erdos142.r_three_eq_rothNumberNat

The statement

For every natural number $N$ (an explicit universally quantified variable; there are no hypotheses of any kind, and no typeclass assumptions beyond those baked into the two definitions below), the claim is the equality of two natural numbers:

$$r(3, N) \;=\; \mathrm{rothNumberNat}(N).$$

Both sides are natural numbers, so this is an equation in $\mathbb{N}$. Everything hinges on what the two sides unfold to, so each is expanded in full below.

The left-hand side: $r(3,N)$

$r$ is a bundle-local (non-standard, non-Mathlib) function $r : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ defined by

$$r(k,N) \;=\; \sup\Bigl\{\, |S| \;\Big|\; S \subseteq \{1,2,\dots,N\} \text{ a finite set, and } S \text{ is "}k\text{-AP-free" in the bundle's sense} \,\Bigr\},$$

where $S$ ranges over finite subsets of $\mathbb{N}$, the ambient interval is the closed integer interval $\{1,2,\dots,N\}$ (note: it starts at $1$, and it is empty when $N = 0$), $|S|$ is the number of elements of $S$, and the supremum is the supremum of a set of natural numbers taken in the conditionally complete lattice $\mathbb{N}$. That last point carries the usual junk-value convention: if the set of cardinalities were empty or unbounded above, the supremum would be $0$ by fiat. Here neither degeneracy arises for a genuine reason — the empty set always qualifies, contributing the value $0$, and every $S$ satisfies $|S| \le N$ — so the supremum is an attained maximum. The definition is marked noncomputable.

The freeness condition, again bundle-local, is the following chain of definitions, instantiated at $k = 3$ (the natural number $3$ is coerced into $\mathbb{N}\cup\{\infty\}$, the type in which the "length" parameter lives).

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

$$\mathrm{IsAPOfLengthWith}(s, l, a, d) \;:\iff\; \bigl(\#s = l\bigr) \;\wedge\; \Bigl( s = \{\, a + n\cdot d \;:\; n \in \mathbb{N},\ n < l \,\} \Bigr),$$

where $\#s$ denotes the cardinality of $s$ as an element of $\mathbb{N}\cup\{\infty\}$ (equal to $\infty$ when $s$ is infinite), $n \cdot d$ is the $n$-fold monoid multiple of $d$, and $n < l$ compares the coerced natural $n$ with $l$ in $\mathbb{N}\cup\{\infty\}$.

$$\mathrm{IsAPOfLength}(s,l) \;:\iff\; \exists\, a,\ \exists\, d,\ \mathrm{IsAPOfLengthWith}(s,l,a,d).$$

Note that $d$ is not required to be nonzero here; the constraint $\#s = l$ is the only thing that can force distinctness.

$$\mathrm{IsAPOfLengthFree}(s,l) \;:\iff\; \forall\, t \subseteq s,\ \ \mathrm{IsAPOfLength}(t,l) \;\Rightarrow\; l \le 1 .$$

The conclusion of that implication is a statement about $l$ alone, not about $t$ or $s$. Consequently: when $l \le 1$ the predicate holds vacuously for every $s$; when $l \ge 2$ — in particular for the value $l = 3$ used here — the conclusion is false, so the predicate says exactly that no subset $t \subseteq s$ satisfies $\mathrm{IsAPOfLength}(t,l)$.

Putting this together for $l = 3$ over $\mathbb{N}$: a finite set $S \subseteq \{1,\dots,N\}$ is counted by $r(3,N)$ exactly when there is no subset $t$ of (the underlying set of) $S$ and no pair $a, d \in \mathbb{N}$ with

$$\#t = 3 \quad\text{and}\quad t = \{a + 0\cdot d,\ a + 1\cdot d,\ a + 2\cdot d\} = \{a,\ a+d,\ a+2d\}.$$

Because the cardinality of $t$ is required to be exactly $3$, the difference $d$ is forced to be nonzero (in $\mathbb{N}$, $\{a, a+d, a+2d\}$ has three elements only if $d \neq 0$), and the three terms are the set $\{a, a+d, a+2d\}$ — the pattern is captured up to set equality, not as an ordered triple. So $r(3,N)$ is the largest size of a subset of $\{1,\dots,N\}$ containing no three distinct elements forming an arithmetic progression $a, a+d, a+2d$ with $d > 0$.

The right-hand side: $\mathrm{rothNumberNat}(N)$

This is the Mathlib declaration rothNumberNat, a bundled monotone map $\mathbb{N} \to \mathbb{N}$, applied to $N$. It is defined as the additive Roth number of the finite set $\mathrm{range}(N) = \{0, 1, \dots, N-1\}$ — note this interval starts at $0$ and ends at $N-1$, and is empty when $N = 0$. Unfolding the additive Roth number:

$$\mathrm{rothNumberNat}(N) \;=\; \mathrm{findGreatest}\Bigl(\ m \mapsto \exists\, t \subseteq \{0,\dots,N-1\},\ |t| = m \ \wedge\ \mathrm{ThreeAPFree}(t)\ ,\ \ N \Bigr),$$

where $\mathrm{findGreatest}(P, n)$ denotes the largest $m \le n$ satisfying $P(m)$, and $0$ if no such $m$ exists (the bound $n$ here is $|\mathrm{range}(N)| = N$). Since the predicate holds at $m = 0$ via the empty set, this is the largest $m \le N$ for which some $m$-element $3$-AP-free subset of $\{0,\dots,N-1\}$ exists.

Mathlib's $3$-AP-freeness predicate for a set $s$ of naturals is:

$$\mathrm{ThreeAPFree}(s) \;:\iff\; \forall\, a \in s,\ \forall\, b \in s,\ \forall\, c \in s,\quad a + c = b + b \;\Longrightarrow\; a = b.$$

(The three membership arguments and $a$, $b$, $c$ themselves are strict-implicit binders; the conclusion is literally $a = b$.) This formulation admits the degenerate solution $a = b = c$, and it is stated over the coercion of the finite set $t$ to a set.

What the equality therefore asserts

For every natural $N$, the largest cardinality of a subset of $\{1, 2, \dots, N\}$ having no subset that is a $3$-element arithmetic progression $\{a, a+d, a+2d\}$ equals the largest $m \le N$ such that $\{0, 1, \dots, N-1\}$ has an $m$-element subset $t$ with the property that $a, b, c \in t$ and $a + c = 2b$ together imply $a = b$.

The two sides are computed over different ground intervals: $\{1,\dots,N\}$ on the left and $\{0,\dots,N-1\}$ on the right. Both are empty when $N = 0$, in which case the equation reads $0 = 0$.

Notes on the surrounding bundle

The bundle also defines the predicates

$$\mathrm{HasAP}(k, A) \;:\iff\; \exists\, a, d \in \mathbb{N},\ d > 0 \ \wedge\ \forall\, i < k,\ a + i\,d \in A, \qquad \mathrm{APFree}(k,A) :\iff \neg\,\mathrm{HasAP}(k,A),$$

and proves three auxiliary facts (the empty set is $\mathrm{IsAPOfLengthFree}$ for every length; every progression-free $S \subseteq \{1,\dots,N\}$ satisfies $|S| \le r(k,N)$; and $r(k,N) \le N$). Neither $\mathrm{HasAP}$ nor $\mathrm{APFree}$ appears in the statement being read back, and $\mathrm{HasAP}$ as written asks only for membership of the terms $a + i\,d$ in $A$, without requiring them to be distinct or to exhaust $A$.

The proof body of the theorem is a placeholder (sorry); nothing about the truth of the equality is established by this file.