Read-back: Erdos142.apFree_iff

The statement

The declaration fixes a natural number $k$, a hypothesis $2 \le k$, and a finite set $A$ of natural numbers ($A$ is a Finset ℕ, so it is finite by construction and its elements are natural numbers, including possibly $0$). It asserts a biconditional (an "if and only if", in both directions) between two separate custom predicates defined in the accompanying bundle:

$$\mathrm{APFree}(k, A) \iff \mathrm{IsAPOfLengthFree}(\widehat{A},\, \hat{k})$$

Here $\widehat{A}$ denotes the underlying set of naturals obtained by coercing the finite set $A$ to a plain set, and $\hat{k}$ denotes the image of $k$ under the coercion $\mathbb{N} \to \mathbb{N} \cup \{\infty\}$ into the extended natural numbers $\mathbb{N}^\infty$ (which has a top element $\infty$ in addition to all naturals).

No proof is supplied: the body is a sorry placeholder.

Both sides are custom notions, expanded separately below. They are not stated in terms of each other; they are two independently written definitions.

Left-hand side: $\mathrm{APFree}(k, A)$ — the "elementary" side

$\mathrm{APFree}(k, A)$ is defined as the negation of another custom predicate $\mathrm{HasAP}(k, A)$, which reads:

$$\mathrm{HasAP}(k, A) \;:=\; \exists\, a, d \in \mathbb{N},\quad 0 < d \ \wedge\ \bigl(\forall i \in \mathbb{N},\ i < k \Rightarrow a + i \cdot d \in A\bigr).$$

So the left-hand side of the equivalence literally says:

$$\mathrm{APFree}(k, A) \;:=\; \neg\,\exists\, a, d \in \mathbb{N} \ \bigl[\, 0 < d \ \wedge\ \forall i < k,\ a + i\,d \in A \,\bigr],$$

i.e. there is no pair of natural numbers $a$ (first term) and $d$ (common difference) with $d$ strictly positive such that all $k$ values $a,\ a+d,\ a+2d,\ \dots,\ a+(k-1)d$ are members of $A$.

Points that the quantifiers silently include:

• $a$ ranges over all of $\mathbb{N}$, so $a = 0$ is allowed; $d$ ranges over $\mathbb{N}$ but is constrained by $0 < d$, so $d = 0$ is excluded on this side.
• The index condition is $i < k$ over natural numbers $i$, i.e. $i \in \{0, 1, \dots, k-1\}$; membership is required for every such $i$.
• The condition is stated as membership of the $k$ values $a + i\,d$ in $A$; it does not by itself speak of a $k$-element subset. (Since $d > 0$, the listed values are pairwise distinct, but the definition never says this.)
• The product is $i \cdot d$ in $\mathbb{N}$; no subtraction or division occurs, so there are no truncation or junk-value effects.
• $A$ is finite, so for $k$ this side is a statement about finitely many candidate pairs $(a,d)$ only in effect, not by stipulation: $a$ and $d$ are quantified over all of $\mathbb{N}$.

Right-hand side: $\mathrm{IsAPOfLengthFree}(\widehat{A}, \hat{k})$ — the "set/cardinality" side

This side is built from a chain of three definitions, stated in the bundle for an arbitrary additive commutative monoid $\alpha$ and here instantiated at $\alpha = \mathbb{N}$.

(1) Progression with prescribed data. For a set $s \subseteq \alpha$, a length $l \in \mathbb{N}^\infty$, and elements $a, d \in \alpha$:

$$\mathrm{IsAPOfLengthWith}(s, l, a, d) \;:=\; \bigl(\mathrm{card}^\infty(s) = l\bigr)\ \wedge\ \Bigl(s = \{\, a + n \bullet d \ :\ n \in \mathbb{N},\ n < l \,\}\Bigr),$$

where $\mathrm{card}^\infty(s)$ is the cardinality of $s$ measured in $\mathbb{N}^\infty$ (equal to $\infty$ when $s$ is infinite), $n \bullet d$ is the $n$-fold monoid multiple of $d$ (for $\alpha = \mathbb{N}$ this is just $n \cdot d$), and $n < l$ compares the coerced natural $n$ with $l$ in $\mathbb{N}^\infty$. Note this is a conjunction of two conditions: the cardinality must equal $l$ and the set must be exactly equal (not merely contained in) the displayed image set.

(2) Progression. For $s$ and $l$:

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

Here $d$ is not required to be nonzero, and $a$ is unrestricted.

(3) Progression-freeness. For $s$ and $l$:

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

The quantifier ranges over all subsets $t$ of $s$ (arbitrary sets, not just finite ones, though here $s = \widehat{A}$ is finite so every $t$ is finite). The consequent $l \le 1$ is an inequality in $\mathbb{N}^\infty$ about the length parameter $l$ itself — it says nothing about $t$.

Putting the three together, the right-hand side of the equivalence literally asserts:

$$\forall\, t \subseteq \widehat{A},\quad \Bigl[\ \exists\, a, d \in \mathbb{N}:\ \mathrm{card}^\infty(t) = \hat{k}\ \wedge\ t = \{\, a + n\,d \ :\ n \in \mathbb{N},\ n < k \,\}\ \Bigr] \ \Longrightarrow\ \hat{k} \le 1 .$$

Points that the quantifiers silently include:

• Because the hypothesis $2 \le k$ is assumed in the theorem, the consequent $\hat{k} \le 1$ is false. Consequently, under that hypothesis, the right-hand side holds exactly when the antecedent is never satisfiable, i.e. when no subset $t$ of $A$ has exactly $k$ elements and is simultaneously equal to the set $\{\,a + n d : n < k\,\}$ for some naturals $a$ and $d$.
• $d = 0$ is permitted in the existential. With $d = 0$ the displayed set is $\{a\}$ (for $k \ge 1$), whose cardinality is $1$, so the cardinality clause $\mathrm{card}^\infty(t) = \hat{k}$ would fail for $k \ge 2$; but the definition itself imposes no positivity on $d$.
• The requirement is a set equality $t = \{a + n d : n < k\}$ together with an exact cardinality $\mathrm{card}^\infty(t) = \hat{k}$, not a containment.
• The empty subset $t = \emptyset$ is included in the range of $\forall t$; its cardinality is $0$, which equals $\hat{k}$ only when $k = 0$ (excluded here by $2 \le k$).
• $A$ itself is among the subsets $t$ considered.
• $\hat{k}$ is a coerced natural, hence never $\infty$; the $l = \infty$ case allowed by the general definitions does not arise in this statement.

Scope of the claim

• The equivalence is asserted only under the hypothesis $2 \le k$; the statement says nothing about $k = 0$ or $k = 1$.
• It is asserted for every finite set $A \subseteq \mathbb{N}$, including $A = \emptyset$ and singletons.
• The ambient type is fixed to $\mathbb{N}$ on both sides; the general monoid $\alpha$ of the bundle definitions plays no role beyond instantiation.
• The remaining declarations in the bundle — the quantity $r(k,N)$ (defined as the supremum of the cardinalities of subsets $S \subseteq \{1,\dots,N\}$ satisfying $\mathrm{IsAPOfLengthFree}(\widehat{S}, \hat{k})$), and the auxiliary results that $\emptyset$ is progression-free, that $|S| \le r(k,N)$ for progression-free $S \subseteq \{1,\dots,N\}$, and that $r(k,N) \le N$ — do not appear in this statement.