TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-08 (gpt-5.6-terra-codex-subscription)

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.

$\mathbb{R}((t^{-1}))$ is an ordered field, ordered by the sign of the leading coefficient

Statement

Let $K = \mathbb{R}((t^{-1}))$ and let $P = \{\, f \in K : f \ne 0_K \text{ and } \operatorname{lc}(f) > 0 \,\}$ (The formal Laurent series $\mathbb{R}((t^{-1}))$ : support bounded below, valuation, leading coefficient). Then:

$P$ is a positive cone on $K$ , so $(K, P)$ is an ordered field (Ordered field), and $f < g$ holds exactly when $g - f \ne 0_K$ and $\operatorname{lc}(g - f) > 0$ .
For $f \ne 0_K$ the absolute value (Absolute value in an ordered field) satisfies $|f| \ne 0_K$ , $v(|f|) = v(f)$ and $\operatorname{lc}(|f|) = \lvert \operatorname{lc}(f) \rvert > 0$ .
The map $\iota : \mathbb{R} \to K$ sending $c$ to the series with value $c$ at index $0$ is an injective ring homomorphism with $\iota(c) \in P$ exactly when $c > 0$ ; and the canonical naturals of $K$ are $n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}})$ for every $n \in \mathbb{N}$ .

Facts & Assumptions

Given: $K$ with its valuation $v$ , leading coefficient $\operatorname{lc}$ , constants $\iota(c)$ and the set $P$ above.

[L1]

For nonzero $h \in K$ , $h(k) = 0$ for $k < v(h)$ and $h(v(h)) = \operatorname{lc}(h) \ne 0$ ; $\iota(c)$ is $c$ at index $0$ and $0$ elsewhere; $1_K = \iota(1)$ (The formal Laurent series $\mathbb{R}((t^{-1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$K$ is a commutative ring, $(f+g)(k) = f(k)+g(k)$ , and $(\iota(c)h)(k) = c\,h(k)$ ( $\mathbb{R}((t^{-1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below).

[L3]

For nonzero $f, g \in K$ : $fg \ne 0_K$ with $\operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g)$ ; $-f \ne 0_K$ with $v(-f) = v(f)$ and $\operatorname{lc}(-f) = -\operatorname{lc}(f)$ ; if $v(f) < v(g)$ then $f+g \ne 0_K$ with $v(f+g) = v(f)$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f)$ ; and if $v(f) = v(g)$ with $\operatorname{lc}(f) + \operatorname{lc}(g) \ne 0$ then $f+g \ne 0_K$ with $\operatorname{lc}(f+g) = \operatorname{lc}(f) + \operatorname{lc}(g)$ (Valuation and leading coefficient in $\mathbb{R}((t^{-1}))$ : $v(fg) = v(f) + v(g)$ , and the behaviour of $v$ under sums).

[L4]

$K$ is a field ( $\mathbb{R}((t^{-1}))$ is a field: every nonzero formal Laurent series is invertible, Field).

[L5]

An ordered field is a field with a subset $P$ satisfying (O1) trichotomy, for each $x$ exactly one of $x \in P$ , $x = 0$ , $-x \in P$ , and (O2) closure of $P$ under addition and multiplication; the order is then $a < b :\iff b - a \in P$ (Ordered field). For $n \ge 1$ , $n \cdot 1_F$ is the $n$ -fold sum of $1_F$ , and $0 \cdot 1_F = 0$ (Archimedean ordered field).

[L6]

$\mathbb{R}$ is an ordered field: exactly one of $x > 0$ , $x = 0$ , $x < 0$ holds for each real $x$ , and sums and products of positive reals are positive (The reals form a totally ordered field, Ordered field).

[L7]

$|x| = x$ when $x \ge 0$ and $|x| = -x$ when $x < 0$ , in any ordered field and in $\mathbb{R}$ (Absolute value in an ordered field).

[L8]

Induction: a property holding at $0$ and inherited from $n$ to $n+1$ holds at every natural number (The principle of mathematical induction, The natural numbers $\mathbb{N}$ (von Neumann)).

[L9]

The order on $\mathbb{Z}$ is total, so for $p, q \in \mathbb{Z}$ exactly one of $p < q$ , $p = q$ , $q < p$ holds (The integers form a totally ordered ring).

Proof

technique · direct

1.1

Let $f \in K$ . If $f = 0_K$ then neither $f$ nor $-f = 0_K$ lies in $P$ , since membership in $P$ requires being nonzero. If $f \ne 0_K$ then $-f \ne 0_K$ and $\operatorname{lc}(-f) = -\operatorname{lc}(f)$ by [L3], and by trichotomy in $\mathbb{R}$ ([L6]) exactly one of $\operatorname{lc}(f) > 0$ and $-\operatorname{lc}(f) > 0$ holds. So for every $f$ exactly one of $f \in P$ , $f = 0_K$ , $-f \in P$ holds, which is (O1).

L1L3L5L6

1.2

Let $f, g \in P$ . By [L3] $fg \ne 0_K$ and $\operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g)$ , a product of two positive reals, hence positive by [L6]; so $fg \in P$ .

L3L6

1.3

$\iota(c) + \iota(d) = \iota(c+d)$ because addition is computed index by index, and $\iota(c)\iota(d) = \iota(cd)$ because $(\iota(c)\iota(d))(k) = c\,\iota(d)(k)$ by [L2], which is $cd$ at $k = 0$ and $0$ elsewhere; also $\iota(1) = 1_K$ , and $\iota$ is injective since $\iota(c)(0) = c$ .

L1L2

2.1

Let $f, g \in P$ and compare $v(f)$ with $v(g)$ , which by [L9] are related in exactly one of three ways. If $v(f) < v(g)$ then by [L3] $f + g \ne 0_K$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f) > 0$ ; if $v(g) < v(f)$ the same argument with the roles exchanged applies; and if $v(f) = v(g)$ then $\operatorname{lc}(f) + \operatorname{lc}(g) > 0$ by [L6], in particular nonzero, so by [L3] $f+g \ne 0_K$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f) + \operatorname{lc}(g) > 0$ . In every case $f + g \in P$ , which with [step 1.2] is (O2).

step 1.2L3L6L9

2.2

For $c \ne 0$ the series $\iota(c)$ is nonzero with $v(\iota(c)) = 0$ and $\operatorname{lc}(\iota(c)) = c$ , so $\iota(c) \in P$ exactly when $c > 0$ ; and $\iota(0) = 0_K \notin P$ . With [step 1.3] this makes $\iota$ an injective ring homomorphism carrying the positive reals onto the positive constants.

step 1.3L1

2.3

For every natural $n$ , $n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}})$ : at $n = 0$ both sides are $0_K$ by [L5] and [L1], and if the identity holds at $n$ then $(n+1)\cdot 1_K = n \cdot 1_K + 1_K = \iota(n \cdot 1_{\mathbb{R}}) + \iota(1) = \iota(n \cdot 1_{\mathbb{R}} + 1) = \iota((n+1)\cdot 1_{\mathbb{R}})$ by [step 1.3].

step 1.3L1L5L8

3.1

By [step 1.1] and [step 2.1] the set $P$ satisfies (O1) and (O2), and $K$ is a field by [L4]; hence $(K,P)$ is an ordered field, in which $f < g$ means $g - f \in P$ , that is, $g - f \ne 0_K$ and $\operatorname{lc}(g-f) > 0$ .

step 1.1step 2.1L4L5

4.1

Let $f \ne 0_K$ . If $f \in P$ then $f > 0_K$ by [step 3.1], so $|f| = f$ by [L7], and $\operatorname{lc}(|f|) = \operatorname{lc}(f) = \lvert \operatorname{lc}(f)\rvert$ since $\operatorname{lc}(f) > 0$ . Otherwise $-f \in P$ by [step 1.1], so $f < 0_K$ and $|f| = -f$ , whence $|f| \ne 0_K$ , $v(|f|) = v(f)$ and $\operatorname{lc}(|f|) = -\operatorname{lc}(f) = \lvert\operatorname{lc}(f)\rvert$ , again positive. In both cases $v(|f|) = v(f)$ and $\operatorname{lc}(|f|) = \lvert\operatorname{lc}(f)\rvert > 0$ .

step 1.1step 3.1L3L7

5.1

Clause 1 is [step 3.1], clause 2 is [step 4.1], and clause 3 is [step 2.2] with [step 2.3].

step 3.1step 2.2step 4.1step 2.3∎

Remarks

The order compares lowest terms, and only those. By clause 1, deciding $f < g$ means finding the least index at which $f$ and $g$ differ and comparing the two coefficients there. Every later coefficient is irrelevant, which is why $\iota(c) > t^{-1}$ for every positive real $c$ , however small, and why the order is not the coefficientwise one.
$\mathbb{R}$ sits inside $K$ as an ordered subfield, and that is all clause 3 says. It does not say that $\mathbb{R}$ is cofinal in $K$ , and indeed it is not: the computation used for the canonical naturals in $\mathbb{R}((t^{-1}))$ is non-Archimedean, and the monomials $t^{-k}$ are cofinal below its positive elements applies verbatim to every constant, since $v(t) = -1 < 0 = v(\iota(c))$ for every $c \ne 0$ , so $\iota(c) < t$ for every real $c$ . The identification $n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}})$ is recorded because the Archimedean property is a statement about the canonical naturals (Archimedean ordered field), and it is the bridge between those and the constant series.

Depends on

Used by

Cited to discharge well-definedness by The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 68 results over 30 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Ordered field (Wikipedia) (standard reference, not scraped)
Hahn series (Wikipedia) (standard reference, not scraped)
H. G. Dales, Norming infinitesimals of large fields (standard reference, not scraped)

R((t−1))\mathbb{R}((t^{-1}))R((t−1)) is an ordered field, ordered by the sign of the leading coefficient