The subsets of $\mathbb{N}$ containing a tail form the Fréchet filter, and it is proper and not an ultrafilter

The family ${\mathcal{B}}_{\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{l}}$ is nonempty because it contains $T_0=\mathbb{N}$, and every $T_k$ is nonempty because $k\in T_k$ by reflexivity of $\le$.

For $k,\mathrm{\ell }\in \mathbb{N}$, totality gives $k\le \mathrm{\ell }$ or $\mathrm{\ell }\le k$; in the first case $T_{\mathrm{\ell }}\subseteq T_k\cap T_{\mathrm{\ell }}$, and in the second $T_k\subseteq T_k\cap T_{\mathrm{\ell }}$. Thus the tails are downward directed and none is empty.

Every finite list of natural numbers has a strict upper bound: the empty list is bounded by $0$, and if $b$ strictly bounds the first $r$ entries, totality compares $b$ with the last entry $s(r)$, after which the successor of the larger one strictly bounds all $\sigma (r)$ entries; induction proves the assertion for every length $r$.

If $T_k\subseteq A$, then $\mathbb{N}\setminus A\subseteq k=\{0,\dots ,k-1\}$, so the complement is contained in the range of the finite identity list $i\mapsto i$ on $k$.

Let $E:=\{r+r:r\in \mathbb{N}\}$. For every $k$, the natural $k+k$ belongs to $E\cap T_k$, because $k\le k+k$ by the order definition with gap $k$.

For every $k$, the successor $\sigma (k+k)=k+k+1$ does not belong to $E$: if $r+r=\sigma (k+k)$, then totality gives $r\le k$ or $k<r$ after separating the equality case; in the first case addition compatibility gives $r+r\le k+k$, contradicting $k+k<\sigma (k+k)$, while in the second it gives $k+k<k+r<r+r=\sigma (k+k)$, contradicting the immediacy of the successor.

For each $k$, if $n\in T_{\sigma (k)}$ then $k<n$ by [L4], so $n\mathrm{\ne }k$; hence $T_{\sigma (k)}\subseteq \mathbb{N}\setminus \{k\}$ and $\mathbb{N}\setminus \{k\}\in {\mathcal{F}}_{\mathrm{F}\mathrm{r}}$.

For every $k$, one has $k\le k+k<\sigma (k+k)$, so step 1.6 gives an element of $T_k\setminus E$.

By steps 1.1 and 1.2, ${\mathcal{B}}_{\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{l}}$ is a filter base, and [L1] makes its upward closure ${\mathcal{F}}_{\mathrm{F}\mathrm{r}}$ a proper filter.

Conversely, if $\mathbb{N}\setminus A$ is contained in the range of a finite list, choose a strict upper bound $k$ for that list by step 1.3. Then no $n\ge k$ lies in $\mathbb{N}\setminus A$, so $T_k\subseteq A$ and $A\in {\mathcal{F}}_{\mathrm{F}\mathrm{r}}$.

Steps 1.4 and 2.3 show that $A\in {\mathcal{F}}_{\mathrm{F}\mathrm{r}}$ exactly when $\mathbb{N}\setminus A$ is finite, so the tail and cofinite descriptions agree.

Steps 1.5 and 2.1 show that every tail meets both $E$ and $\mathbb{N}\setminus E$. Therefore neither $E$ nor its complement contains a tail, so neither belongs to ${\mathcal{F}}_{\mathrm{F}\mathrm{r}}$.

Since ${\mathcal{F}}_{\mathrm{F}\mathrm{r}}$ contains neither member of the complementary pair $E,\mathbb{N}\setminus E$, [L2] shows that it is not an ultrafilter. Together with step 2.2, this proves that the Fréchet filter is proper but not ultra.