ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passverified 2026-08-13 (gpt-5.6-sol-codex-subscription)↗ rests on later material (inherited)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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

Example

Let $R (t)$ be the field of fractions (For a field $F$ , $F (t) = Frac (F [t])$ is its rational function field; in particular $R (t) = Frac (R [t])$ ) of the polynomial ring $R [t]$ , and let

$P = {f \in R (t) : f \neq 0 and f (x) > 0 for all sufficiently large real x} .$

Not every ordered field is Archimedean proves that $(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:

A computation rule. For $f = p / q$ with $p, q \in R [t]$ nonzero, $f \in P$ exactly when $lc (p) lc (q) > 0$ , where $lc$ is the leading coefficient. So comparing two rational functions is comparing one product of two real numbers.
That the rule is independent of the representative $p / q$ chosen, which is what makes it a definition of a function on $R (t)$ and not merely on pairs.
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).

Facts & Assumptions

Given: The field $R (t)$ of fractions of $R [t]$ , whose elements are written $p / q$ with $p, q \in R [t]$ and $q \neq 0$ , with $p / q = p^{'} / q^{'}$ exactly when $p q^{'} = p^{'} q$ ; and the set $P$ above. For a nonzero $p \in R [t]$ , $lc (p)$ denotes its leading coefficient.

[L1]

$(R (t), P)$ is an ordered field, and $n \cdot 1 < t$ for every natural $n$ , so it is not Archimedean (Not every ordered field is Archimedean, Ordered field, Archimedean ordered field).

[L2]

For a commutative ring $R$ and a nonzero $f \in R [x]$ , $\deg f$ is the largest index carrying a nonzero coefficient and $lc (f)$ is that coefficient (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree). For a field $F$ the polynomial ring $F [t]$ is an integral domain (For a field $F$ , $F (t) = Frac (F [t])$ is its rational function field; in particular $R (t) = Frac (R [t])$ ), and $R$ is a field (The reals form a totally ordered field, Field). If $R$ is an integral domain and $f, g \in R [x]$ are nonzero, then $f g \neq 0$ , $\deg (f g) = \deg f + \deg g$ and $lc (f g) = lc (f) lc (g)$ (Over an integral domain, degrees add under multiplication of nonzero polynomials).

[L3]

In $R$ , a nonzero square is positive (Squares of nonzero elements are positive); a product of two nonzero reals is positive exactly when both are positive or both are negative (Sign rules for products and monotonicity of multiplication).

[L4]

In an ordered field, $f < g$ means $g - f \in P$ ; a positive element has a positive inverse (Inverses of positives are positive, and reciprocation reverses order, Ordered field).

[L5]

The canonical embedding of $Q$ into an ordered field is an order embedding, so a rational $q > 0$ names a positive element $q \cdot 1$ of $R (t)$ (The unique embedding of ℚ into an ordered field).

[L6]

In an ordered field $∣ u ∣ = u$ when $u \geq 0$ and $∣ u ∣ = - u$ when $u < 0$ (Absolute value in an ordered field), and $- ∣ u ∣ \leq u \leq ∣ u ∣$ for every $u$ (Basic properties of the absolute value); $R$ is a totally ordered field (The reals form a totally ordered field).

Verification

technique · direct

1.1

Let $p \in R [t]$ be nonzero, with $m = \deg p$ and $a = lc (p) \neq 0$ , so that $p (x) = a x^{m} + \sum_{i < m} a_{i} x^{i}$ for every real $x$ . If $m = 0$ then $p (x) = a$ for every $x$ . If $m \geq 1$ , put $C = \sum_{i < m} ∣ a_{i} ∣ \geq 0$ ; for $x \geq 1$ and $i < m$ one has $0 < x^{i} \leq x^{m - 1}$ , and $- ∣ a_{i} ∣ \leq a_{i} \leq ∣ a_{i} ∣$ , so $- ∣ a_{i} ∣ x^{m - 1} \leq a_{i} x^{i} \leq ∣ a_{i} ∣ x^{m - 1}$ , and adding these $m$ inequalities gives $- C x^{m - 1} \leq \sum_{i < m} a_{i} x^{i} \leq C x^{m - 1}$ . Hence if $a > 0$ then $p (x) \geq a x^{m} - C x^{m - 1} = x^{m - 1} (a x - C) > 0$ for every $x > \max (1, C / a)$ ; and if $a < 0$ , the same bound applied to $- p$ , whose leading coefficient is $- a > 0$ , gives $p (x) < 0$ for every $x > \max (1, C / (- a))$ . In every case there is a real $X_{p}$ such that $p (x) \neq 0$ and $p (x)$ has the sign of $lc (p)$ for every $x > X_{p}$ .

givenL2L3L6algebra

1.2

If $p / q = p^{'} / q^{'}$ then $p q^{'} = p^{'} q$ , so $lc (p) lc (q^{'}) = lc (p^{'}) lc (q)$ ; multiplying both sides by $lc (q) lc (q^{'})$ gives $lc (p) lc (q) \cdot lc (q^{'})^{2} = lc (p^{'}) lc (q^{'}) \cdot lc (q)^{2}$ , and both squares are positive, so $lc (p) lc (q)$ and $lc (p^{'}) lc (q^{'})$ have the same sign.

L2L3

2.1

For nonzero $p, q \in R [t]$ put $X = \max (X_{p}, X_{q})$ with $X_{p}, X_{q}$ as in step 1.1: for every $x > X$ neither $p$ nor $q$ vanishes, so $f = p / q$ has a value $f (x) = p (x) / q (x)$ there, and since $p (x)$ has the sign of $lc (p)$ and $q (x)$ the sign of $lc (q)$ , the sign of that value is the sign of $lc (p) lc (q)$ ; hence $f \in P$ exactly when $lc (p) lc (q) > 0$ .

step 1.1L3

3.1

The rule of step 2.1 is therefore independent of the representative and computes membership in $P$ ; combined with [L1] it computes the order: $p / q < p^{'} / q^{'}$ exactly when the numerator and denominator of $p^{'} / q^{'} - p / q$ , written in any representative, have leading coefficients of positive product.

step 1.2step 2.1L1L4

3.2

$1 / t \in P$ , since $lc (1) lc (t) = 1 > 0$ ; equivalently, $t \in P$ and inverses of positives are positive.

step 2.1L3L4

4.1

For every rational $q > 0$ : $q \cdot 1 - 1 / t = (q t - 1) / t$ , whose leading coefficients have product $q \cdot 1 = q > 0$ , so $1 / t < q \cdot 1$ . Together with step 3.2, $0 < 1 / t < q \cdot 1$ for every positive rational $q$ .

step 2.1step 3.1step 3.2L3L5

4.2

For every natural $n$ : $t - n \cdot 1$ has leading coefficients with product $1 > 0$ , so $n \cdot 1 < t$ ; and $t^{2} - t = t (t - 1)$ likewise gives $t < t^{2}$ .

step 2.1step 3.1L2L3

5.1

So $R (t)$ is an ordered field, computed by a single product of leading coefficients, in which $t$ is larger than every canonical natural and $1 / t$ is a positive infinitesimal.

step 3.1step 4.1step 4.2L1∎

Remarks

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 $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 $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 $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 $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 $R ((t^{- 1}))$ , which is why that field was built ( $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 $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.

Depends on

Used by

In ℝ(t) the rationals are not dense: no rational lies strictly between 0 and 1/t Counterexample

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

D. J. Eck, Axioms for the Real Numbers (standard reference, not scraped)
Ordered field (Wikipedia) (standard reference, not scraped)
Field of fractions (Wikipedia) (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)

The rational function field R(t)R(t) ordered by the eventual sign is an ordered field, worked out