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{tail}}$ 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,\ell\in\mathbb N$, totality gives $k\le\ell$ or $\ell\le k$; in the first case $T_\ell\subseteq T_k\cap T_\ell$, and in the second $T_k\subseteq T_k\cap T_\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,\ldots,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\neq k$; hence $T_{\sigma(k)}\subseteq\mathbb N\setminus\{k\}$ and $\mathbb N\setminus\{k\}\in\mathcal F_{\mathrm{Fr}}$.

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{tail}}$ is a filter base, and [L1] makes its upward closure $\mathcal F_{\mathrm{Fr}}$ 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{Fr}}$.

Steps 1.4 and 2.3 show that $A\in\mathcal F_{\mathrm{Fr}}$ 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{Fr}}$.

Since $\mathcal F_{\mathrm{Fr}}$ 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.