TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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.

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

Statement

Let $K = R ((t^{- 1}))$ and let $P = {f \in K : f \neq 0_{K} and lc (f) > 0}$ (The formal Laurent series $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 \neq 0_{K}$ and $lc (g - f) > 0$ .
For $f \neq 0_{K}$ the absolute value (Absolute value in an ordered field) satisfies $∣ f ∣ \neq 0_{K}$ , $v (∣ f ∣) = v (f)$ and $lc (∣ f ∣) = ∣ lc (f) ∣ > 0$ .
The map $ι : R \to K$ sending $c$ to the series with value $c$ at index $0$ is an injective ring homomorphism with $ι (c) \in P$ exactly when $c > 0$ ; and the canonical naturals of $K$ are $n \cdot 1_{K} = ι (n \cdot 1_{R})$ for every $n \in N$ .

Facts & Assumptions

Given: $K$ with its valuation $v$ , leading coefficient $lc$ , constants $ι (c)$ and the set $P$ above.

[L1]

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

[L2]

$K$ is a commutative ring, $(f + g) (k) = f (k) + g (k)$ , and $(ι (c) h) (k) = c h (k)$ ( $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$ : $f g \neq 0_{K}$ with $lc (f g) = lc (f) lc (g)$ ; $- f \neq 0_{K}$ with $v (- f) = v (f)$ and $lc (- f) = - lc (f)$ ; if $v (f) < v (g)$ then $f + g \neq 0_{K}$ with $v (f + g) = v (f)$ and $lc (f + g) = lc (f)$ ; and if $v (f) = v (g)$ with $lc (f) + lc (g) \neq 0$ then $f + g \neq 0_{K}$ with $lc (f + g) = lc (f) + lc (g)$ (Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums).

[L4]

$K$ is a field ( $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 : ⟺ b - a \in P$ (Ordered field). For $n \geq 1$ , $n \cdot 1_{F}$ is the $n$ -fold sum of $1_{F}$ , and $0 \cdot 1_{F} = 0$ (Archimedean ordered field).

[L6]

$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 \geq 0$ and $∣ x ∣ = - x$ when $x < 0$ , in any ordered field and in $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 $N$ (von Neumann)).

[L9]

The order on $Z$ is total, so for $p, q \in 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 \neq 0_{K}$ then $- f \neq 0_{K}$ and $lc (- f) = - lc (f)$ by [L3], and by trichotomy in $R$ ([L6]) exactly one of $lc (f) > 0$ and $- 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] $f g \neq 0_{K}$ and $lc (f g) = lc (f) lc (g)$ , a product of two positive reals, hence positive by [L6]; so $f g \in P$ .

L3L6

1.3

$ι (c) + ι (d) = ι (c + d)$ because addition is computed index by index, and $ι (c) ι (d) = ι (c d)$ because $(ι (c) ι (d)) (k) = c ι (d) (k)$ by [L2], which is $c d$ at $k = 0$ and $0$ elsewhere; also $ι (1) = 1_{K}$ , and $ι$ is injective since $ι (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 \neq 0_{K}$ and $lc (f + g) = lc (f) > 0$ ; if $v (g) < v (f)$ the same argument with the roles exchanged applies; and if $v (f) = v (g)$ then $lc (f) + lc (g) > 0$ by [L6], in particular nonzero, so by [L3] $f + g \neq 0_{K}$ and $lc (f + g) = lc (f) + lc (g) > 0$ . In every case $f + g \in P$ , which with [step 1.2] is (O2).

step 1.2L3L6L9

2.2

For $c \neq 0$ the series $ι (c)$ is nonzero with $v (ι (c)) = 0$ and $lc (ι (c)) = c$ , so $ι (c) \in P$ exactly when $c > 0$ ; and $ι (0) = 0_{K} \notin P$ . With [step 1.3] this makes $ι$ 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} = ι (n \cdot 1_{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} = ι (n \cdot 1_{R}) + ι (1) = ι (n \cdot 1_{R} + 1) = ι ((n + 1) \cdot 1_{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 \neq 0_{K}$ and $lc (g - f) > 0$ .

step 1.1step 2.1L4L5

4.1

Let $f \neq 0_{K}$ . If $f \in P$ then $f > 0_{K}$ by [step 3.1], so $∣ f ∣ = f$ by [L7], and $lc (∣ f ∣) = lc (f) = ∣ lc (f) ∣$ since $lc (f) > 0$ . Otherwise $- f \in P$ by [step 1.1], so $f < 0_{K}$ and $∣ f ∣ = - f$ , whence $∣ f ∣ \neq 0_{K}$ , $v (∣ f ∣) = v (f)$ and $lc (∣ f ∣) = - lc (f) = ∣ lc (f) ∣$ , again positive. In both cases $v (∣ f ∣) = v (f)$ and $lc (∣ f ∣) = ∣ lc (f) ∣ > 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 $ι (c) > t^{- 1}$ for every positive real $c$ , however small, and why the order is not the coefficientwise one.
$R$ sits inside $K$ as an ordered subfield, and that is all clause 3 says. It does not say that $R$ is cofinal in $K$ , and indeed it is not: the computation used for the canonical naturals in $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 (ι (c))$ for every $c \neq 0$ , so $ι (c) < t$ for every real $c$ . The identification $n \cdot 1_{K} = ι (n \cdot 1_{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 · two levels

40 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

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))R((t−1)) is an ordered field, ordered by the sign of the leading coefficient