The rational function field $\mathbb{R}(t)$ ordered by the eventual sign is an ordered field, worked out

Let $\mathbb{R}(t)$ be the field of fractions of the polynomial ring $\mathbb{R}[t]$, and let

$P \;=\; \{\, f \in \mathbb{R}(t) : f \ne 0 \text{ and } f(x) > 0 \text{ for all sufficiently large real } x \,\}.$

Not every ordered field is Archimedean proves that $(\mathbb{R}(t), P)$ is an ordered field and that it is not Archimedean. This example works the order out in usable form. Three things are established below:

1. A computation rule. For $f = p/q$ with $p, q \in \mathbb{R}[t]$ nonzero, $f \in P$ exactly when $\operatorname{lc}(p)\operatorname{lc}(q) > 0$, where $\operatorname{lc}$ is the leading coefficient. So comparing two rational functions is comparing one product of two real numbers.
2. That the rule is independent of the representative $p/q$ chosen, which is what makes it a definition of a function on $\mathbb{R}(t)$ and not merely on pairs.
3. The two elements that make the field interesting: $t$, which exceeds every canonical natural, and $1/t$, which is positive and lies below every positive rational. An element of the second kind is called an infinitesimal, and its existence is exactly the failure of the Archimedean property (Archimedean ordered field).

• Why the eventual sign, and not the sign at a point. Evaluating at a fixed real $x_0$ is not even a function on all of $\mathbb{R}(t)$, since a rational function may have a pole at $x_0$; and even where evaluation is defined, its sign cannot give a positive cone on the field, because the nonzero rational function $t-x_0$ evaluates to $0$, so trichotomy fails. The behaviour at $+\infty$ is one representative-independent, multiplicative choice, and step 1.1 is exactly that statement.

• What this field is and is not good for. It is the library's cheapest witness that an ordered field need not be Archimedean, and In $\mathbb{R}(t)$ the rationals are not dense: no rational lies strictly between $0$ and $1/t$ uses the infinitesimal $1/t$ found above to show $\mathbb{Q}$ need not be dense. It is not a witness for the completeness failures of FALSE: the nested interval property alone implies the least-upper-bound property or FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property: nothing in this library proves that $\mathbb{R}(t)$ is Cauchy complete or that it has any nested interval property, and in fact it is neither. Those two need the larger field $\mathbb{R}((t^{-1}))$, which is why that field was built ($\mathbb{R}((t^{-1}))$, the formal Laurent series field, is Cauchy complete, non-Archimedean, and lacks the least-upper-bound property).

• The order is the one induced from $\mathbb{R}((t^{-1}))$ in spirit but not by any embedding proved here. Both fields order an element by its behaviour at infinity, and in both the comparison looks at a single coefficient. This library constructs no embedding of one into the other and never uses one.