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.

✓ 9 results · all verified · 6 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Formal Laurent Series Field $R ((t^{- 1}))$ : Cauchy Complete, Non-Archimedean, Not Complete

1 · Prerequisites

2 · Summary

Objective. This page builds one field and proves five things about it, because the five together are a single fact that no earlier page in this library could exhibit: Cauchy completeness does not imply the least-upper-bound property. The field is $K = R ((t^{- 1}))$ , the formal Laurent series in $t^{- 1}$ over $R$ , and what is proved here is that $K$ is an ordered field, that it is not Archimedean, that it therefore fails the least-upper-bound property, that every Cauchy sequence in it nevertheless converges, and that it satisfies the nested interval property in the shrinking form. The last two hold in a field where the first three fail, and that is the whole point.

Why a new field, when $R (t)$ was already available. Not every ordered field is Archimedean built the rational functions ordered by eventual sign and used them for exactly one purpose: to show that an ordered field need not be Archimedean. That is the whole of what this library has proved about $R (t)$ , and it is not enough here, because nothing there speaks about Cauchy sequences or about nested intervals; this page does not settle either question for $R (t)$ and does not need to. $K$ is built instead, and every property required below is proved for it outright. The two fields are ordered by the same idea, the behaviour of an element at infinity, but an element of $K$ is an arbitrary series in descending powers of $t$ rather than a ratio of polynomials. This page does not construct an embedding of $R (t)$ into $K$ and never uses one; the relationship is recorded honestly in the remarks of The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient and is not relied on anywhere.

The construction, and the one hard algebraic step. The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient defines an element of $K$ as a function $Z \to R$ whose support is bounded below, written $\sum_{k \geq k_{0}} a_{k} t^{- k}$ , with the valuation $v (f)$ its lowest nonzero index and $lc (f)$ the coefficient there. $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below does the bookkeeping that makes the definition legitimate: bounded-below support is exactly what makes each coefficient of a product a finite sum, it is preserved by both operations, and the result is a commutative ring. Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums then records the two facts that every later argument runs on, $v (f g) = v (f) + v (g)$ and the behaviour of $v$ under sums, from which $K$ is at once an integral domain.

The genuinely non-trivial algebra is $R ((t^{- 1}))$ is a field: every nonzero formal Laurent series is invertible: every nonzero series is invertible. The obstacle is that the natural formula for the inverse is a geometric series, and $K$ has no notion of an infinite sum. What replaces it is the observation that $u^{n}$ vanishes at every index below $n$ when $u$ does below $1$ , so at any single index only finitely many powers contribute; the inverse is defined index by index from that finite truncation, and the fact that the result again has support bounded below is checked rather than assumed. That check is where a hand-waved proof would fail.

The order, and where it stops behaving like $R$ . $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient orders $K$ by the sign of the leading coefficient: $f > 0$ exactly when the lowest-index nonzero coefficient of $f$ is a positive real. Comparison therefore looks at one coefficient only, the first at which two elements differ, and every later coefficient is irrelevant. That single sentence explains everything unusual about $K$ . $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements draws the consequences: $t$ exceeds every canonical natural, so $K$ is not Archimedean; the monomials $t^{- k}$ decrease; and, the clause that matters most, every positive element of $K$ exceeds some $t^{- k}$ with $k \in N$ . The value group is $Z$ , whose cofinality is countable, and that clause is what countable cofinality means down in the order.

$R ((t^{- 1}))$ does not have the least-upper-bound property; its canonical naturals have no supremum is then two lines of abstract nonsense and a short concrete argument. The abstract route is the contrapositive of Every complete ordered field is Archimedean, proved several pages earlier: a complete ordered field is Archimedean, $K$ is not, so $K$ is not complete. The concrete route names the set that fails, the canonical naturals ${n \cdot 1_{K}}$ , which are bounded above by $t$ and have no least upper bound because every upper bound of them can be halved at its leading coefficient and remain an upper bound. Both are kept, because a reader who is about to be told that $K$ is Cauchy complete is entitled to see precisely which set has no supremum.

Sequences in a field that is not $R$ . Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field is deliberately general: it fixes convergence, Cauchyness, monotonicity, boundedness, subsequences and closed intervals in an arbitrary ordered field $F$ , so that the later page on the equivalent forms of completeness has one place to cite rather than a reconstruction of its own. Two points in it are load bearing rather than decorative. The thresholds $ε$ range over $F$ , not over the rationals, and in a non-Archimedean field that is a real difference: this page contains a sequence that would pass the Cauchy test read with rational thresholds and fails it in $K$ . And a theorem proved about sequences of reals is a theorem about $R$ ; it may not be cited for a general $F$ merely because its proof looks like it would transfer.

Cauchy completeness, and why the argument is not a formality. Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete is the main theorem. Its hinge is the countable-cofinality clause of $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements: the continuum of thresholds in the Cauchy condition collapses to the countable family $t^{- k}$ , so testing against those suffices, and a sequence indexed by $N$ is long enough to meet all of them. Applying the condition at $t^{- (k + 1)}$ says that the coefficients at all indices $j \leq k$ are eventually constant along the sequence, and the limit is assembled from those eventual values. Two obligations are discharged explicitly rather than waved through: the assembled function must have support bounded below, which comes from the single threshold $k = 0$ freezing the entire negative half-line at one stage; and no choice is used, since each stage is defined as a least element supplied by the well-ordering principle rather than chosen.

Nested intervals, in one form and not the other. $R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$ deduces from Cauchy completeness that a nested sequence of closed intervals whose lengths tend to $0$ in the order of $K$ meets in exactly one point. The restriction is not a weakness of the proof. The unrestricted property is false in $K$ , and The unrestricted nested interval property fails in $R ((t^{- 1}))$ exhibits nested intervals $[ι (n) t^{- 1}, ι (1 / (n + 1))]$ with empty intersection: a common point would have to be infinitesimal, because it lies below every positive real constant, and simultaneously larger than every multiple of $t^{- 1}$ , which no element of $K$ is. The shrinking hypothesis must also be read in $K$ and not in $R$ , and both items say so. The lengths in the counterexample keep a nonzero coefficient at index $0$ , so not one of them ever gets below $t^{- 1}$ ; and the remarks of $R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$ make the same point with lengths that are the real constants $2 / (n + 1)$ , which tend to $0$ in the ordinary real sense and do not tend to $0$ in $K$ at all.

What this page is for. Three results elsewhere in the library need a single honest witness, and this field is it: an ordered field in which every Cauchy sequence converges but the least-upper-bound property fails; an ordered field with the shrinking nested interval property but without least upper bounds; and a Cauchy complete, non-Archimedean, incomplete ordered field. All three are statements about the same $K$ , and every ingredient of all three is proved on this page.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient

Definition

Throughout, $R$ is the field of real numbers with its order (The real numbers, The reals form a totally ordered field) and $Z$ is the totally ordered commutative ring of integers (The integers as equivalence classes of pairs of naturals, Arithmetic on the integers, Order on the integers, The integers form a totally ordered ring).

For a function $f : Z \to R$ write

$supp f : = {k \in Z : f (k) \neq 0},$

and say that $supp f$ is bounded below when there is $m \in Z$ with $f (k) = 0$ for every $k < m$ . The set of formal Laurent series in $t^{- 1}$ over $R$ is

$K = R ((t^{- 1})) : = {f : Z \to R ∣ supp f is bounded below},$

equipped with

$(f + g) (k) : = f (k) + g (k), (f g) (k) : = \sum_{i + j = k} f (i) g (j),$

where the product sum ranges over the pairs $(i, j) \in Z \times Z$ with $i + j = k$ and $f (i) g (j) \neq 0$ . That set of pairs is finite for every $k$ , and $f + g$ and $f g$ again lie in $K$ : this is $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗, which also proves that $K$ with these operations is a commutative ring whose zero $0_{K}$ is the constant function $0$ and whose identity $1_{K}$ is the function taking the value $1$ at $0$ and $0$ elsewhere.

Distinguished elements. For $n \in Z$ let $t^{- n} \in K$ be the function taking the value $1$ at $n$ and $0$ at every other index; so $t^{0} = 1_{K}$ , and $t : = t^{- (- 1)}$ is the function taking the value $1$ at $- 1$ . For $c \in R$ let $ι (c) \in K$ be the function taking the value $c$ at $0$ and $0$ elsewhere. The notation $t^{- n}$ is defined here as a name; that it is consistent with the ring multiplication, $t^{- m} t^{- n} = t^{- (m + n)}$ , is proved in $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗.

Series notation. Because $supp f$ is bounded below, say by $m$ , one writes

$f = \sum_{k \geq m} f (k) t^{- k},$

a purely notational device: the object is the function $f$ , and no convergence of any kind is asserted or used.

Valuation and leading coefficient. Let $f \in K$ with $f \neq 0_{K}$ . Then $supp f$ is nonempty and bounded below, so it has a least element ( $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗). Define

$v (f) : = \min supp f \in Z, lc (f) : = f (v (f)) \in R ∖ {0} .$

$v (f)$ is the valuation and $lc (f)$ the leading coefficient of $f$ . Neither is defined at $f = 0_{K}$ , whose support is empty; every statement about $v$ or $lc$ in this library carries the hypothesis $f \neq 0_{K}$ explicitly.

Order. The positive cone of $K$ is

$P : = {f \in K : f \neq 0_{K} and lc (f) > 0},$

that is, a nonzero series is positive exactly when its lowest-index nonzero coefficient is a positive real. That $(K, P)$ is an ordered field (Ordered field, Field) is $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient ↗, and that every nonzero element of $K$ is invertible is $R ((t^{- 1}))$ is a field: every nonzero formal Laurent series is invertible ↗. As in any ordered field, $f < g$ means $g - f \in P$ .

Remarks

Why the support must be bounded below. It is exactly what makes the product a finite sum. If arbitrary functions $Z \to R$ were admitted, the defining sum for $(f g) (k)$ would range over an infinite set of pairs and would denote nothing, since $K$ carries no notion of convergence. The condition is preserved by both operations, which is the content of $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗.
Indices run over all of $Z$ , and the edge cases are real. The zero series has empty support and no valuation. A nonzero constant series $ι (c)$ has $v (ι (c)) = 0$ and $lc (ι (c)) = c$ , so the index $k = 0$ is an ordinary index and not a boundary. Negative indices are admitted, and they are what makes $t = t^{- (- 1)}$ , whose support is ${- 1}$ , an element of $K$ ; a series may have finitely many terms of negative index but never infinitely many.
The order is not the coefficientwise order. Two series are compared by their lowest differing coefficient, not by all of them at once, and this is what makes $t^{- 1}$ smaller than every positive real constant while $t$ is larger than every real constant. The consequences are drawn in $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements.
Relation to the rational functions. The ordered field $R (t)$ of Not every ordered field is Archimedean, ordered so that $f > 0$ exactly when $f (x) > 0$ for all sufficiently large real $x$ , is the standard first example of a non-Archimedean ordered field, and standard treatments identify it with a subfield of $K$ by expanding each rational function at infinity. This page neither constructs that identification nor uses it, and no item here may be cited for it: everything proved about $K$ below is proved from the definition above and nothing else. What the two objects share, and all that is used here, is the idea of ordering by behaviour at infinity.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

$R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Statement

Let $K = R ((t^{- 1}))$ be as in The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient, and let $f, g \in K$ , with $m, n \in Z$ chosen so that $f (i) = 0$ for all $i < m$ and $g (j) = 0$ for all $j < n$ . Then:

(Finiteness.) For every $k \in Z$ the set $S_{k} : = {(i, j) \in Z \times Z : i + j = k, f (i) g (j) \neq 0}$ is finite, so $(f g) (k) = \sum_{i + j = k} f (i) g (j)$ is a finite sum of reals; and $S_{k} = \emptyset$ whenever $k < m + n$ .
(Closure.) $f + g$ , $- f$ and $f g$ lie in $K$ , with $(f + g) (k) = 0$ for $k < \min (m, n)$ and $(f g) (k) = 0$ for $k < m + n$ .
(Ring.) $(K, +, \cdot, 0_{K}, 1_{K})$ is a commutative ring with identity, and $1_{K} \neq 0_{K}$ .
(Monomials and constants.) $(t^{- a} h) (k) = h (k - a)$ for every $h \in K$ and all $a, k \in Z$ ; consequently $t^{- a} t^{- b} = t^{- (a + b)}$ for all $a, b \in Z$ . Moreover $(ι (c) f) (k) = c f (k)$ for all $c \in R$ and $k \in Z$ .
(Least element.) Every nonempty $S \subseteq Z$ that is bounded below has a least element. In particular $supp f$ has a least element whenever $f \neq 0_{K}$ , so the valuation $v (f)$ and the leading coefficient $lc (f)$ of The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient are defined.

Facts & Assumptions

Given: $K$ , its operations, $0_{K}$ , $1_{K}$ , the monomials $t^{- n}$ and the constants $ι (c)$ as in The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient; elements $f, g \in K$ and bounds $m, n \in Z$ with $f (i) = 0$ for $i < m$ and $g (j) = 0$ for $j < n$ .

[L1]

$K$ consists of the functions $Z \to R$ whose support is bounded below; $(f + g) (k) = f (k) + g (k)$ and $(f g) (k) = \sum_{i + j = k} f (i) g (j)$ ; $0_{K}$ is the zero function, $1_{K}$ is $1$ at index $0$ and $0$ elsewhere, $t^{- a}$ is $1$ at index $a$ and $0$ elsewhere, and $ι (c)$ is $c$ at index $0$ and $0$ elsewhere (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$Z$ is a totally ordered commutative ring: its order is total, and $x \leq y$ implies $x + z \leq y + z$ (The integers form a totally ordered ring, Order on the integers, Arithmetic on the integers).

[L3]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L4]

The map $ε (a) = [(a, 0)]$ is injective from $N$ onto the set of nonnegative integers and preserves addition and order, so every integer $x \geq 0$ is $ε (a)$ for a unique natural $a$ (The naturals embed in the integers).

[L5]

$R$ is a field: addition and multiplication are associative and commutative, multiplication distributes over addition, $0 \neq 1$ , and a finite sum of reals is independent of the order and bracketing of its terms (Field, The reals form a totally ordered field).

Proof

technique · direct

1.1

Let $S \subseteq Z$ be nonempty with $s \geq b$ for all $s \in S$ . Every element of $T : = {s - b : s \in S}$ is a nonnegative integer, so by [L4] $T = {ε (a) : a \in A}$ for a nonempty $A \subseteq N$ ; by [L3] $A$ has a least element $a_{0}$ , and since $ε$ preserves order and $x \mapsto x + b$ preserves order, $ε (a_{0}) + b$ is an element of $S$ that is $\leq$ every element of $S$ .

L2L3L4

1.2

Fix $k \in Z$ and let $(i, j) \in S_{k}$ . Then $f (i) \neq 0$ and $g (j) \neq 0$ , so $i \geq m$ and $j \geq n$ ; from $i + j = k$ and $j \geq n$ we get $i = k - j \leq k - n$ . Hence $m \leq i \leq k - n$ , and $j = k - i$ is determined by $i$ .

givenL1L2

2.1

The integers $i$ with $m \leq i \leq k - n$ are in order-preserving bijection with the naturals $a$ satisfying $ε (a) \leq k - n - m$ by [L4], and there are finitely many of these, none at all when $k - n - m < 0$ ; so $S_{k}$ is a finite set by [step 1.2], it is empty whenever $k < m + n$ , and therefore $(f g) (k)$ is a finite sum of reals which is $0$ whenever $k < m + n$ .

step 1.2L2L4L5

3.1

$(f + g) (k) = f (k) + g (k) = 0$ for every $k < \min (m, n)$ and $(- f) (k) = - f (k) = 0$ for every $k < m$ , so $f + g$ and $- f$ have support bounded below; and $(f g) (k) = 0$ for every $k < m + n$ by [step 2.1], so $f g$ does too. All three therefore lie in $K$ .

step 2.1givenL1L5

3.2

$(f g) (k) = \sum_{i + j = k} f (i) g (j) = \sum_{j + i = k} g (j) f (i) = (g f) (k)$ , since the two sums have the same finite index set and their terms agree by commutativity of multiplication in $R$ ; so multiplication on $K$ is commutative.

step 2.1L5

3.3

For $f, g, h \in K$ and $k \in Z$ , expanding both $((f g) h) (k)$ and $(f (g h)) (k)$ by [L1] and [L5] gives the sum of $f (i) g (j) h (l)$ over the triples $(i, j, l)$ with $i + j + l = k$ and $f (i) g (j) h (l) \neq 0$ ; that set is finite because the argument of [step 1.2] bounds $i$ , $j$ and $l$ from below and hence, as in [step 2.1], from above as well. So multiplication on $K$ is associative.

step 1.2step 2.1L5

3.4

$(f (g + h)) (k) = \sum_{i + j = k} f (i) (g (j) + h (j)) = \sum_{i + j = k} f (i) g (j) + \sum_{i + j = k} f (i) h (j) = (f g) (k) + (f h) (k)$ , all three sums being finite; so multiplication distributes over addition.

step 2.1L5

3.5

For $h \in K$ , $(t^{- a} h) (k) = \sum_{i + j = k} t^{- a} (i) h (j)$ has at most one nonzero term, the one with $i = a$ and $j = k - a$ , so $(t^{- a} h) (k) = h (k - a)$ ; taking $h = t^{- b}$ gives $(t^{- a} t^{- b}) (k) = t^{- b} (k - a)$ , which is $1$ when $k = a + b$ and $0$ otherwise, that is, $t^{- a} t^{- b} = t^{- (a + b)}$ .

step 2.1L1

3.6

$(ι (c) f) (k) = \sum_{i + j = k} ι (c) (i) f (j)$ has at most one nonzero term, the one with $i = 0$ and $j = k$ , so $(ι (c) f) (k) = c f (k)$ .

step 2.1L1

3.7

$(f \cdot 1_{K}) (k) = \sum_{i + j = k} f (i) 1_{K} (j)$ has at most one nonzero term, the one with $j = 0$ and $i = k$ , so $(f \cdot 1_{K}) (k) = f (k)$ and $f \cdot 1_{K} = f$ ; moreover $1_{K} (0) = 1 \neq 0 = 0_{K} (0)$ , so $1_{K} \neq 0_{K}$ .

step 2.1L1L5

4.1

Addition on $K$ is defined index by index, and $K$ is closed under it and under negation by [step 3.1]; so associativity, commutativity, the law $f + 0_{K} = f$ and the law $f + (- f) = 0_{K}$ each hold at every index by the corresponding law in $R$ , and $(K, +, 0_{K})$ is an abelian group.

step 3.1L1L5

5.1

By [step 4.1] addition makes $K$ an abelian group, by [step 3.2], [step 3.3] and [step 3.7] multiplication is commutative and associative with identity $1_{K} \neq 0_{K}$ , and by [step 3.4] it distributes over addition; hence $K$ is a commutative ring with identity.

step 3.2step 3.3step 3.4step 3.7step 4.1

6.1

Clause 1 is [step 2.1], clause 2 is [step 3.1] with [step 2.1], clause 3 is [step 5.1], clause 4 is [step 3.5] and [step 3.6], and clause 5 is [step 1.1] applied to $S = supp f$ , which is nonempty when $f \neq 0_{K}$ and bounded below because $f \in K$ .

step 1.1step 2.1step 3.1step 3.5step 3.6step 5.1∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums

Statement

Let $K = R ((t^{- 1}))$ with its valuation $v$ and leading coefficient $lc$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient), and let $f, g \in K$ with $f \neq 0_{K}$ and $g \neq 0_{K}$ . Then:

(Products.) $f g \neq 0_{K}$ , and $v (f g) = v (f) + v (g), lc (f g) = lc (f) lc (g) .$ In particular $K$ has no zero divisors.
(Negatives.) $- f \neq 0_{K}$ , $v (- f) = v (f)$ and $lc (- f) = - lc (f)$ .
(Unequal valuations.) If $v (f) < v (g)$ then $f + g \neq 0_{K}$ , $v (f + g) = v (f)$ and $lc (f + g) = lc (f)$ .
(Equal valuations, no cancellation.) If $v (f) = v (g) = q$ and $lc (f) + lc (g) \neq 0$ , then $f + g \neq 0_{K}$ , $v (f + g) = q$ and $lc (f + g) = lc (f) + lc (g)$ .
(Sums in general.) If $f + g \neq 0_{K}$ then $v (f + g) \geq \min {v (f), v (g)}$ .

Facts & Assumptions

Given: $f, g \in K$ with $f \neq 0_{K}$ and $g \neq 0_{K}$ ; write $p : = v (f)$ and $q : = v (g)$ .

[L1]

For a nonzero $h \in K$ one has $h (k) = 0$ for every $k < v (h)$ and $h (v (h)) = lc (h) \neq 0$ ; conversely, if $h (k) = 0$ for all $k < r$ and $h (r) \neq 0$ then $h \neq 0_{K}$ , $v (h) = r$ and $lc (h) = h (r)$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$(f + g) (k) = f (k) + g (k)$ and $(f g) (k) = \sum_{i + j = k} f (i) g (j)$ , a finite sum; if $f$ vanishes at every index below $m$ and $g$ at every index below $n$ , then $f g$ vanishes at every index below $m + n$ ( $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below, The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L3]

$R$ is a field, so a product of two nonzero reals is nonzero, and $- x = 0$ only for $x = 0$ (Field, The reals form a totally ordered field).

[L4]

The order on $Z$ is total and compatible with addition (The integers form a totally ordered ring, Order on the integers).

Proof

technique · direct

1.1

By [L1] $f$ vanishes at every index below $p$ and $g$ at every index below $q$ , so by [L2] $(f g) (k) = 0$ for every $k < p + q$ .

L1L2

1.2

If $(i, j)$ satisfies $i + j = p + q$ and $f (i) g (j) \neq 0$ then $i \geq p$ and $j \geq q$ by [L1], and $i + j = p + q$ then forces $i = p$ and $j = q$ ; hence $(f g) (p + q) = f (p) g (q) = lc (f) lc (g)$ , which is nonzero by [L3].

L1L2L3L4

1.3

$(- f) (k) = - f (k)$ for every $k$ , so $- f$ vanishes exactly where $f$ does; by [L1] and [L3] this gives $- f \neq 0_{K}$ , $v (- f) = p$ and $lc (- f) = - lc (f) \neq 0$ .

L1L2L3

1.4

Suppose $p < q$ . For $k < p$ both $f (k) = 0$ and $g (k) = 0$ , so $(f + g) (k) = 0$ ; and $g (p) = 0$ because $p < q$ , so $(f + g) (p) = lc (f) \neq 0$ . By [L1], $f + g \neq 0_{K}$ with $v (f + g) = p$ and $lc (f + g) = lc (f)$ .

L1L2L4

1.5

Suppose $p = q$ and $lc (f) + lc (g) \neq 0$ . For $k < p$ both terms vanish, so $(f + g) (k) = 0$ ; and $(f + g) (p) = lc (f) + lc (g) \neq 0$ . By [L1], $f + g \neq 0_{K}$ , $v (f + g) = p$ and $lc (f + g) = lc (f) + lc (g)$ .

L1L2

1.6

For $k < \min {p, q}$ one has $f (k) = g (k) = 0$ , hence $(f + g) (k) = 0$ ; so if $f + g \neq 0_{K}$ then its valuation, being the least index at which it is nonzero, satisfies $v (f + g) \geq \min {p, q}$ .

L1L2L4

2.1

By [step 1.1] $f g$ vanishes at every index below $p + q$ and by [step 1.2] it is nonzero at $p + q$ ; so by [L1] $f g \neq 0_{K}$ , $v (f g) = p + q$ and $lc (f g) = lc (f) lc (g)$ . Since $f$ and $g$ were arbitrary nonzero elements, no product of nonzero elements of $K$ is zero.

step 1.1step 1.2L1

3.1

Clause 1 is [step 2.1], clause 2 is [step 1.3], clause 3 is [step 1.4], clause 4 is [step 1.5] and clause 5 is [step 1.6].

step 1.3step 1.4step 1.5step 1.6step 2.1∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

$R ((t^{- 1}))$ is a field: every nonzero formal Laurent series is invertible

Statement

$K = R ((t^{- 1}))$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient) is a field (Field): it is a commutative ring with $1_{K} \neq 0_{K}$ , and every $f \in K$ with $f \neq 0_{K}$ has a multiplicative inverse in $K$ .

Explicitly, if $p = v (f)$ and $c = lc (f)$ , then $f = ι (c) t^{- p} (1_{K} - u)$ for the element $u \in K$ given by $u (j) = - c^{- 1} f (p + j)$ for $j \geq 1$ and $u (j) = 0$ for $j \leq 0$ , and $f^{- 1} = ι (c^{- 1}) t^{p} g$ , where $g \in K$ vanishes at every index $< 0$ and is given at $k \geq 0$ by $g (k) = \sum_{n = 0}^{k} (u^{n}) (k)$ .

Scratch work

The identity behind the construction is the geometric series $(1 - u)^{- 1} = 1 + u + u^{2} + \dots$ . It cannot be used as written, because $K$ has no notion of an infinite sum. What replaces it is the observation that $u^{n}$ vanishes at every index below $n$ , so at any single index $k$ only the terms $n \leq k$ can contribute; the displayed formula for $g (k)$ is that finite truncation, and the support of the result is bounded below because every $u^{n}$ vanishes below $0$ .

Facts & Assumptions

Given: A nonzero $f \in K$ ; write $p : = v (f) \in Z$ and $c : = lc (f) \in R ∖ {0}$ , so that $f (k) = 0$ for every $k < p$ and $f (p) = c$ .

[L1]

$K$ is the set of functions $Z \to R$ whose support is bounded below; $t^{- a}$ is $1$ at index $a$ and $0$ elsewhere; $ι (c)$ is $c$ at index $0$ and $0$ elsewhere; for nonzero $h \in K$ one has $h (k) = 0$ for $k < v (h)$ and $h (v (h)) = lc (h) \neq 0$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$K$ is a commutative ring with identity $1_{K} \neq 0_{K}$ ; $(h_{1} h_{2}) (k) = \sum_{i + j = k} h_{1} (i) h_{2} (j)$ is a finite sum; if $h_{1}$ vanishes at every index $< a$ and $h_{2}$ at every index $< b$ then $h_{1} h_{2}$ vanishes at every index $< a + b$ ; $(t^{- a} h) (k) = h (k - a)$ and hence $t^{- a} t^{- b} = t^{- (a + b)}$ ; 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]

A product of two nonzero elements of $K$ is nonzero (Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums).

[L4]

$R$ is a field: every nonzero $c$ has an inverse $c^{- 1}$ with $c c^{- 1} = 1$ , and a finite sum of reals may be reordered and regrouped freely (Field, The reals form a totally ordered field).

[L5]

Recursion on $N$ : for a set $A$ , an element $a \in A$ and a function $F : A \to A$ there is a unique $Γ : N \to A$ with $Γ (0) = a$ and $Γ (σ (n)) = F (Γ (n))$ (The recursion theorem, The natural numbers $N$ (von Neumann)).

[L6]

Induction: a property holding at $0$ and inherited from $n$ to $σ (n)$ holds at every natural number (The principle of mathematical induction).

[L7]

A field is a commutative ring with $0 \neq 1$ in which multiplication restricted to the nonzero elements is an abelian group, that is, in which the nonzero elements are closed under multiplication and each has an inverse (Field).

Proof

technique · constructive

1.1

Define $u : Z \to R$ by $u (j) : = - c^{- 1} f (p + j)$ for $j \geq 1$ and $u (j) : = 0$ for $j \leq 0$ . Then $u$ vanishes at every index $< 1$ , so its support is bounded below and $u \in K$ .

givenL1L4construct

1.2

By [L5] with $A = K$ , $a = 1_{K}$ and $F (h) = h u$ there is a family $(u^{n})_{n \in N}$ in $K$ with $u^{0} = 1_{K}$ and $u^{σ (n)} = u^{n} u$ .

L2L5construct

2.1

For every $k \in Z$ , $(ι (c) t^{- p} (1_{K} - u)) (k) = c (1_{K} - u) (k - p)$ by [L2]; this is $0$ when $k < p$ because $1_{K} - u$ vanishes at every negative index, it is $c$ when $k = p$ , and it is $c \cdot (- u (k - p)) = c c^{- 1} f (k) = f (k)$ when $k > p$ . Comparing with $f (k) = 0$ for $k < p$ and $f (p) = c$ , we get $f = ι (c) t^{- p} (1_{K} - u)$ .

step 1.1givenL1L2L4

2.2

For every $n \in N$ , $u^{n}$ vanishes at every index $< n$ : at $n = 0$ this says $1_{K}$ vanishes at every negative index, which holds by [L1]; and if $u^{n}$ vanishes at every index $< n$ then, since $u$ vanishes at every index $< 1$ by [step 1.1], the product $u^{σ (n)} = u^{n} u$ vanishes at every index $< n + 1$ by [L2].

step 1.1step 1.2L1L2L6

3.1

Define $g : Z \to R$ by $g (k) : = \sum_{n = 0}^{k} (u^{n}) (k)$ for $k \geq 0$ and $g (k) : = 0$ for $k < 0$ ; each value is a finite sum of reals, and $g$ vanishes at every index $< 0$ , so $g \in K$ .

step 2.2L1L4construct

4.1

Fix $k \geq 1$ . In $(u g) (k) = \sum_{i + j = k} u (i) g (j)$ a term can be nonzero only when $i \geq 1$ and $j \geq 0$ , hence only for $1 \leq i \leq k$ and $j = k - i$ ; so $(u g) (k) = \sum_{i = 1}^{k} u (i) g (k - i) = \sum_{i = 1}^{k} u (i) \sum_{n = 0}^{k - i} (u^{n}) (k - i)$ .

step 1.1step 3.1L1L2

4.2

For $k \leq 0$ one has $(u g) (k) = 0$ , since $u$ vanishes at every index $< 1$ and $g$ at every index $< 0$ , so every pair $(i, j)$ with $i + j = k$ has $u (i) g (j) = 0$ .

step 1.1step 3.1L1L2

5.1

In the inner sum of [step 4.1] the terms with $k - i < n \leq k - 1$ vanish by [step 2.2], so the inner sum may be extended to $n = 0, \dots, k - 1$ without changing its value; interchanging the two finite sums gives $(u g) (k) = \sum_{n = 0}^{k - 1} \sum_{i = 1}^{k} u (i) (u^{n}) (k - i)$ .

step 2.2step 4.1L4

6.1

For each $n$ , $\sum_{i = 1}^{k} u (i) (u^{n}) (k - i) = \sum_{i + j = k} u (i) (u^{n}) (j) = (u u^{n}) (k) = (u^{σ (n)}) (k)$ , because a term of the full convolution can be nonzero only for $i \geq 1$ and $j \geq 0$ ; hence $(u g) (k) = \sum_{n = 0}^{k - 1} (u^{σ (n)}) (k) = \sum_{n = 1}^{k} (u^{n}) (k)$ for every $k \geq 1$ .

step 1.2step 2.2step 5.1L2

7.1

For $k \geq 1$ , $((1_{K} - u) g) (k) = g (k) - (u g) (k) = \sum_{n = 0}^{k} (u^{n}) (k) - \sum_{n = 1}^{k} (u^{n}) (k) = (u^{0}) (k) = 1_{K} (k)$ ; for $k = 0$ , $g (0) = (u^{0}) (0) = 1$ and $(u g) (0) = 0$ , so the value is $1 = 1_{K} (0)$ ; and for $k < 0$ both $g (k)$ and $(u g) (k)$ are $0$ , as is $1_{K} (k)$ . Hence $(1_{K} - u) g = 1_{K}$ .

step 3.1step 4.2step 6.1L1L2

8.1

Using [step 2.1], [L2] and $c c^{- 1} = 1$ , one computes $f \cdot (ι (c^{- 1}) t^{p} g) = ι (c) ι (c^{- 1}) t^{- p} t^{- (- p)} (1_{K} - u) g = 1_{K} \cdot 1_{K} \cdot 1_{K} = 1_{K}$ , so $ι (c^{- 1}) t^{p} g \in K$ is a multiplicative inverse of $f$ .

step 2.1step 7.1L2L4

9.1

$K$ is a commutative ring with $1_{K} \neq 0_{K}$ by [L2], its nonzero elements are closed under multiplication by [L3], and by [step 8.1] every nonzero element has an inverse; so $K$ satisfies the field axioms of [L7] and the construction is complete.

step 8.1L2L3L7discharge-construct∎

Remarks

Where support-boundedness is really used. Twice, and in different ways. It makes each coefficient of a product a finite sum, which is what lets $(u^{n}) (k)$ be spoken of at all; and it is what has to be re-established for the constructed inverse, which is why $g$ was defined to vanish at every negative index rather than found to. The verification that this definition is consistent with $(1_{K} - u) g = 1_{K}$ is [step 7.1], and it is exactly the point at which an infinite geometric series would have had to be summed.
The normalisation is forced, and that is why the recipe is explicit. Suppose $f = ι (c^{'}) t^{- p^{'}} (1_{K} - w)$ with $c^{'} \neq 0$ and $w$ vanishing at every index $\leq 0$ . Evaluating as in [step 2.1] gives $f (k) = c^{'} (1_{K} - w) (k - p^{'})$ , which is $0$ for $k < p^{'}$ and equals $c^{'}$ at $k = p^{'}$ ; so $p^{'} = v (f)$ and $c^{'} = lc (f)$ , and then $w (j) = - c^{' - 1} f (p^{'} + j)$ for $j \geq 1$ . The factorisation used in the proof is therefore the only one of its shape, and the formula for the inverse is a recipe rather than a choice.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-08 (gpt-5.6-terra-codex-subscription)Open item page →

$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.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

$R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements

Statement

Let $K = R ((t^{- 1}))$ be the ordered field of $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient, and identify a natural number with its image in $Z$ when it is used as an index. Then:

$n \cdot 1_{K} < t$ for every $n \in N$ ; consequently $K$ is not Archimedean (Archimedean ordered field).
$0_{K} < t^{- (k + 1)} < t^{- k}$ for every $k \in Z$ .
(Countable cofinality.) For every $ε \in K$ with $ε > 0_{K}$ there is $k \in N$ with $0_{K} < t^{- k} < ε$ ; indeed every integer $k > v (ε)$ works.
(The monomials measure the valuation.) For $h \in K$ and $k \in Z$ : if $h (j) = 0$ for every $j \leq k$ then $∣ h ∣ < t^{- k}$ ; and conversely, if $∣ h ∣ < t^{- k}$ then $h (j) = 0$ for every $j < k$ .

Facts & Assumptions

Given: $K$ with its valuation $v$ , leading coefficient $lc$ , monomials $t^{- a}$ and constants $ι (c)$ .

[L1]

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

[L2]

$K$ is an ordered field in which $f < g$ holds exactly when $g - f \neq 0_{K}$ and $lc (g - f) > 0$ ; for $f \neq 0_{K}$ one has $∣ f ∣ \neq 0_{K}$ , $v (∣ f ∣) = v (f)$ and $lc (∣ f ∣) > 0$ ; and $n \cdot 1_{K} = ι (n \cdot 1_{R})$ , which for $n \geq 1$ is nonzero with $v = 0$ ( $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient, Absolute value in an ordered field).

[L3]

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

[L4]

An ordered field $F$ is Archimedean when for every $x \in F$ there is a natural $n$ with $x < n \cdot 1_{F}$ ; and in an ordered field exactly one of $x < y$ , $x = y$ , $y < x$ holds (Archimedean ordered field, Ordered field).

[L5]

The order on $Z$ is total, and every integer $\geq 0$ is the image of a unique natural number; so for every $m \in Z$ there is a natural $k$ whose image exceeds $m$ (The integers form a totally ordered ring, Order on the integers, The naturals embed in the integers).

Proof

technique · direct

1.1

For every $k \in Z$ the monomial $t^{- k}$ is nonzero with $lc (t^{- k}) = 1 > 0$ , so $t^{- k} > 0_{K}$ by [L2]; and since $v (t^{- k}) = k < k + 1 = v (- t^{- (k + 1)})$ by [L1] and [L3], the difference $t^{- k} - t^{- (k + 1)}$ is nonzero with leading coefficient $lc (t^{- k}) = 1 > 0$ , so $t^{- (k + 1)} < t^{- k}$ .

L1L2L3

1.2

Let $n \in N$ . If $n = 0$ then $t - n \cdot 1_{K} = t$ , which is nonzero with $lc (t) = 1 > 0$ . If $n \geq 1$ then $n \cdot 1_{K}$ is nonzero with $v (n \cdot 1_{K}) = 0$ , so $- (n \cdot 1_{K})$ is nonzero with valuation $0$ by [L3], while $v (t) = - 1 < 0$ ; hence $t - n \cdot 1_{K}$ is nonzero with leading coefficient $lc (t) = 1 > 0$ by [L3]. In both cases $n \cdot 1_{K} < t$ by [L2].

L1L2L3

1.3

Conversely, let $h \in K$ and $k \in Z$ with $∣ h ∣ < t^{- k}$ , and suppose $h \neq 0_{K}$ with $v (h) < k$ . Then $v (∣ h ∣) = v (h) < k = v (t^{- k})$ and $lc (∣ h ∣) > 0$ by [L2], so $∣ h ∣ - t^{- k}$ is nonzero with leading coefficient $lc (∣ h ∣) > 0$ by [L3], giving $t^{- k} < ∣ h ∣$ and contradicting $∣ h ∣ < t^{- k}$ by the trichotomy of [L4]. Hence $h = 0_{K}$ or $v (h) \geq k$ , and in either case $h (j) = 0$ for every $j < k$ by [L1].

L1L2L3L4

2.1

Let $h \in K$ and $k \in Z$ with $h (j) = 0$ for every $j \leq k$ . If $h = 0_{K}$ then $∣ h ∣ = 0_{K} < t^{- k}$ by [step 1.1]. Otherwise $h \neq 0_{K}$ with $v (h) > k$ , so $∣ h ∣ \neq 0_{K}$ with $v (∣ h ∣) = v (h) > k = v (t^{- k})$ by [L1] and [L2]; then $t^{- k} - ∣ h ∣$ is nonzero with leading coefficient $lc (t^{- k}) = 1 > 0$ by [L3], so $∣ h ∣ < t^{- k}$ by [L2].

step 1.1L1L2L3

2.2

Let $ε \in K$ with $ε > 0_{K}$ , so $ε \neq 0_{K}$ and $lc (ε) > 0$ by [L2]; put $m : = v (ε)$ and use [L5] to fix a natural $k$ with $k > m$ . Then $v (ε) = m < k = v (t^{- k}) = v (- t^{- k})$ by [L1] and [L3], so $ε - t^{- k}$ is nonzero with leading coefficient $lc (ε) > 0$ , that is $t^{- k} < ε$ ; and $t^{- k} > 0_{K}$ by [step 1.1]. The same computation applies to every integer $k > m$ .

step 1.1L1L2L3L5

2.3

By [step 1.2], $n \cdot 1_{K} < t$ for every natural $n$ ; by the trichotomy of [L4] no natural $n$ can then satisfy $t < n \cdot 1_{K}$ , so the defining condition of [L4] fails at $x = t$ and $K$ is not Archimedean.

step 1.2L4

3.1

Clause 1 is [step 1.2] with [step 2.3], clause 2 is [step 1.1], clause 3 is [step 2.2], and clause 4 is [step 2.1] together with [step 1.3].

step 1.1step 2.1step 1.3step 2.2step 2.3∎

Remarks

Why clause 3 is the pivotal one. The valuation takes its values in $Z$ , which has countable cofinality, and clause 3 is the translation of that fact into the order of $K$ : a countable family, the monomials $t^{- k}$ with $k \in N$ , already gets below every positive element. This is what makes the sequential Cauchy condition in $K$ testable against countably many thresholds, and it is the reason a sequence indexed by $N$ suffices to reach a limit in Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete. Nothing like it would hold if the exponents were allowed to range over a group of uncountable cofinality.
Non-Archimedean here is a statement about $t$ , not about the constants. The canonical naturals of $K$ are the constant series $n \cdot 1_{K} = ι (n \cdot 1_{R})$ (clause 3 of $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient), all of valuation $0$ , and what bounds them above is $t$ , of valuation $- 1$ . The computation in step 1.2 uses nothing about $t$ beyond that: every positive element of negative valuation exceeds every canonical natural, because a strict inequality between valuations decides the comparison outright, whatever the coefficients are.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

$R ((t^{- 1}))$ does not have the least-upper-bound property; its canonical naturals have no supremum

Statement

$K = R ((t^{- 1}))$ is an ordered field that is not a complete ordered field (Complete ordered field (least-upper-bound property)): it does not have the least-upper-bound property.

The failure is witnessed concretely by the set of canonical naturals $A : = {n \cdot 1_{K} : n \in N} \subseteq K,$ which is nonempty and bounded above by $t$ , yet has no least upper bound in $K$ : every upper bound of $A$ admits a strictly smaller upper bound.

Facts & Assumptions

Given: $K$ with its valuation $v$ , leading coefficient $lc$ , monomials $t^{- a}$ and constants $ι (c)$ ; the set $A = {n \cdot 1_{K} : n \in N}$ .

[L1]

$K$ is an ordered field in which $f < g$ holds exactly when $g - f \neq 0_{K}$ and $lc (g - f) > 0$ ; the canonical naturals are $n \cdot 1_{K} = ι (n \cdot 1_{R})$ ; and for $c \neq 0$ the constant $ι (c)$ is nonzero with $v (ι (c)) = 0$ and $lc (ι (c)) = c$ ( $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient).

[L2]

$n \cdot 1_{K} < t$ for every $n \in N$ , and $K$ is not Archimedean ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements, Archimedean ordered field).

[L3]

Every complete ordered field is Archimedean (Every complete ordered field is Archimedean).

[L4]

$F$ is a complete ordered field when every nonempty $S \subseteq F$ that is bounded above has a least upper bound in $F$ , a least upper bound being an upper bound $\leq$ every upper bound (Complete ordered field (least-upper-bound property)).

[L5]

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

[L6]

For nonzero $f, g \in K$ : $f g \neq 0_{K}$ with $v (f g) = v (f) + v (g)$ and $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 $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 $v (f + g) = v (f)$ and $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).

[L7]

$R$ is a complete ordered field and hence Archimedean: for every real $c$ there is a natural $n$ with $c < n \cdot 1_{R}$ (The reals form a totally ordered field, The Cauchy-sequence reals have the least-upper-bound property, Every complete ordered field is Archimedean).

[L8]

In an ordered field exactly one of $x < y$ , $x = y$ , $y < x$ holds (Ordered field).

Proof

technique · direct

1.1

$K$ is an ordered field that is not Archimedean, while by [L3] every complete ordered field is Archimedean; so $K$ is not a complete ordered field, that is, $K$ does not have the least-upper-bound property of [L4].

L1L2L3L4

1.2

$A$ is nonempty, since $0 \cdot 1_{K} = 0_{K}$ and $1 \cdot 1_{K} = 1_{K}$ lie in it, and it is bounded above by $t$ , since $n \cdot 1_{K} < t$ for every natural $n$ by [L2].

L1L2L4

1.3

Let $s \in K$ be any upper bound of $A$ . Since $1_{K} \in A$ we have $1_{K} \leq s$ , and $1_{K} > 0_{K}$ because $lc (1_{K}) = 1 > 0$ ; so $s > 0_{K}$ , hence $s \neq 0_{K}$ and $lc (s) > 0$ .

L1L4L5

2.1

$v (s) < 0$ . Indeed, if $v (s) > 0$ then $v (1_{K}) = 0 < v (s) = v (- s)$ by [L6], so $1_{K} - s$ is nonzero with leading coefficient $lc (1_{K}) = 1 > 0$ , giving $s < 1_{K}$ and contradicting $1_{K} \leq s$ by [L8]. And if $v (s) = 0$ , write $c : = lc (s) > 0$ and use [L7] to fix a natural $n$ with $c < n \cdot 1_{R}$ ; then $ι (n \cdot 1_{R}) - s$ has both valuations equal to $0$ and leading coefficients summing to $n \cdot 1_{R} - c \neq 0$ , so by [L6] it is nonzero with leading coefficient $n \cdot 1_{R} - c > 0$ , giving $n \cdot 1_{K} > s$ and contradicting that $s$ is an upper bound of $A$ .

step 1.3L1L4L5L6L7L8

3.1

Put $r : = v (s) < 0$ and $c : = lc (s) > 0$ , and set $s^{'} : = ι (c / 2) t^{- r} \in K$ . By [L1], [L5] and [L6], $s^{'}$ is nonzero with $v (s^{'}) = 0 + r = r$ and $lc (s^{'}) = (c / 2) \cdot 1 = c / 2 > 0$ .

step 1.3step 2.1L1L5L6

4.1

$s^{'}$ is an upper bound of $A$ : it satisfies $s^{'} > 0_{K}$ by [L1], which settles $n = 0$ ; and for $n \geq 1$ the element $n \cdot 1_{K}$ is nonzero with valuation $0$ by [L1], so $v (s^{'}) = r < 0 = v (- (n \cdot 1_{K}))$ and [L6] makes $s^{'} - n \cdot 1_{K}$ nonzero with leading coefficient $c / 2 > 0$ , that is $n \cdot 1_{K} < s^{'}$ .

step 3.1L1L5L6

4.2

$s^{'} < s$ : both $s$ and $- s^{'}$ are nonzero of valuation $r$ , and their leading coefficients sum to $c - c / 2 = c / 2 \neq 0$ , so by [L6] the difference $s - s^{'}$ is nonzero with leading coefficient $c / 2 > 0$ .

step 3.1L1L6

5.1

Steps 4.1 and 4.2 show that every upper bound $s$ of $A$ admits an upper bound $s^{'}$ with $s^{'} < s$ , so no upper bound of $A$ is least and $A$ has no least upper bound in $K$ ; with [step 1.2] this exhibits a nonempty subset of $K$ that is bounded above and has no supremum, which is the concrete form of the failure already established in [step 1.1].

step 1.1step 1.2step 4.1step 4.2L4∎

Remarks

Two proofs of one fact, kept apart on purpose. [step 1.1] is the abstract route: non-Archimedean ordered fields cannot be complete, by the contrapositive of Every complete ordered field is Archimedean, and nothing about Laurent series enters it. The rest of the proof is the concrete route, and it names the failing set. Only the concrete route tells the reader what has no supremum, which matters because the same field will be shown to be sequentially Cauchy complete in Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete: the reader is entitled to see the set on which the two notions of completeness disagree.
The halving is not special. Any real $λ$ with $0 < λ < 1$ would serve in place of $1 / 2$ : the only properties used are that $λ c > 0$ , so the smaller element is still positive of valuation $r < 0$ and therefore still above every canonical natural, and that $c - λ c \neq 0$ , so the descent is strict. Both hold for every such $λ$ , which is why the set of upper bounds of $A$ has no least element rather than merely failing to contain one particular candidate.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field

Definition

Throughout, $F$ is an ordered field (Ordered field) with its order and its absolute value $∣ \cdot ∣$ (Absolute value in an ordered field), and $N$ is the set of natural numbers with its order (The natural numbers $N$ (von Neumann), Order on the natural numbers).

A sequence in $F$ is a function $x : N \to F$ . We write $x_{k}$ for $x (k)$ and $(x_{k})$ , or $(x_{k})_{k \in N}$ , for the function itself.

Let $(x_{k})$ be a sequence in $F$ .

$(x_{k})$ is bounded when there is $M \in F$ with $∣ x_{k} ∣ \leq M$ for every $k \in N$ .
$(x_{k})$ converges to $L \in F$ when

$for every ε \in F with ε > 0 there is N \in N such that ∣ x_{k} - L ∣ < ε for all k \geq N .$

We then write $x_{k} \to L$ in $F$ . The sequence is convergent in $F$ when it converges to some $L \in F$ , and divergent in $F$ otherwise.
$(x_{k})$ is Cauchy in $F$ when

$for every ε \in F with ε > 0 there is N \in N such that ∣ x_{k} - x_{l} ∣ < ε for all k, l \geq N .$
$(x_{k})$ is nondecreasing when $x_{j} \leq x_{k}$ for all $j \leq k$ , increasing when $x_{j} < x_{k}$ for all $j < k$ , nonincreasing when $x_{j} \geq x_{k}$ for all $j \leq k$ , decreasing when $x_{j} > x_{k}$ for all $j < k$ , and monotone when it is nondecreasing or nonincreasing.
For a strictly increasing $n : N \to N$ , the subsequence of $(x_{k})$ along $n$ is the composite $(x_{n_{j}})_{j \in N}$ . An element $L \in F$ is a subsequential limit of $(x_{k})$ when some subsequence of $(x_{k})$ converges to $L$ in $F$ .

Closed intervals and nesting. For $a, b \in F$ with $a \leq b$ , the closed interval with endpoints $a$ and $b$ is

$[a, b]_{F} : = {x \in F : a \leq x \leq b},$

and its length is $b - a \geq 0$ . A sequence $(I_{k})_{k \in N}$ of closed intervals $I_{k} = [a_{k}, b_{k}]_{F}$ is nested when $I_{k + 1} \subseteq I_{k}$ for every $k$ . Its lengths tend to $0$ in $F$ when the sequence $(b_{k} - a_{k})_{k \in N}$ converges to $0$ in the sense above, that is, when for every $ε > 0$ in $F$ there is $N \in N$ with $b_{k} - a_{k} < ε$ for all $k \geq N$ (the absolute value may be dropped because each length is $\geq 0$ ).

Remarks

The thresholds range over $F$ , and that is not a stylistic choice. In an Archimedean ordered field one may equivalently test $ε$ over the canonical rationals, and that is what the $R$ -specific Limits and Cauchy sequences of reals does; the two agree there, as the remark on rational and real $ε$ in Sequences of reals: bounded, eventually, frequently, tails, subsequences records. In a general $F$ they do not agree, because the canonical rationals need not be cofinal below the positive elements. A concrete failure lives on this page: in $R ((t^{- 1}))$ every positive rational constant exceeds $t^{- 1}$ (clause 4 of $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements, since a nonzero constant is nonzero at index $0$ ), so the sequence taking the value $0$ at even indices and $t^{- 1}$ at odd indices would satisfy the Cauchy condition read with rational thresholds only, while failing it at $ε = t^{- 2}$ , where consecutive terms differ by $t^{- 1} > t^{- 2}$ ; and it has no limit at all, since a convergent sequence is Cauchy by the triangle inequality. Every definition above therefore quantifies over $ε \in F$ , and no proof in this library may substitute a rational threshold in a field that has not been shown to be Archimedean.
These are the $R$ -notions with $R$ replaced by $F$ , and nothing more. Sequence, tail, subsequence and boundedness are Sequences of reals: bounded, eventually, frequently, tails, subsequences; monotonicity is Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences; subsequential limits are Subsequential limit of a real sequence, and the subsequential limit set; convergence and Cauchyness are Limits and Cauchy sequences of reals; closed intervals are the form $[a, b]$ of Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length. Only the field in which the inequalities are read has changed.
Transfer of theorems is not automatic, and citing an $R$ -item for a general $F$ is a citation error. A result proved about sequences of reals is a statement about $R$ . Many such proofs use only the ordered-field axioms and go through for any $F$ verbatim, and many others use completeness or the Archimedean property and do not. Which is which has to be settled by reading the proof; until an item is stated for a general ordered field, it may not be cited for one.
Limits are unique in any ordered field. If $x_{k} \to L$ and $x_{k} \to L^{'}$ in $F$ with $L \neq L^{'}$ , put $ε : = ∣ L - L^{'} ∣ / 2$ , which is positive because $∣ L - L^{'} ∣ > 0$ (Basic properties of the absolute value) and $2 = 1 + 1 > 0$ . Choose $N$ beyond which both $∣ x_{k} - L ∣ < ε$ and $∣ x_{k} - L^{'} ∣ < ε$ hold, and take any $k \geq N$ : the triangle inequality (The triangle inequality, proved for an arbitrary ordered field) gives $∣ L - L^{'} ∣ \leq ∣ L - x_{k} ∣ + ∣ x_{k} - L^{'} ∣ < 2 ε = ∣ L - L^{'} ∣$ , which is impossible. So the limit, when it exists, is unique, and the notation $\lim_{k} x_{k}$ is unambiguous. No completeness and no Archimedean hypothesis is used.
Indexing starts at $0$ , as everywhere in this library, because $0 \in N$ (The natural numbers $N$ (von Neumann)). A nested sequence of intervals therefore begins with $I_{0}$ , and a statement about "the first $N$ terms" means the indices $0, \dots, N - 1$ .

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-08 (gpt-5.6-terra-codex-subscription)Open item page →

Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete

Statement

Every sequence $(f^{(n)})_{n \in N}$ in $K = R ((t^{- 1}))$ that is Cauchy in $K$ (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field) converges in $K$ . That is, the ordered field $K$ of $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient is sequentially Cauchy complete.

The limit is built coefficient by coefficient: at each index $j \in Z$ the real numbers $f^{(n)} (j)$ are eventually constant in $n$ , and $L (j)$ is that eventual value.

Scratch work

The whole theorem turns on one structural fact about $K$ , and it is worth isolating before the proof: the value group is $Z$ , so it has countable cofinality. Concretely, the countably many monomials $t^{- k}$ , $k \in N$ , get below every positive element of $K$ ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements, clause 3). Two consequences drive everything.

First, the Cauchy condition, which quantifies over the uncountably many positive $ε \in K$ , is equivalent to its restriction to the countable family $ε = t^{- (k + 1)}$ , and by clause 4 of the same lemma that restricted condition says exactly: for each $k$ the coefficients at all indices $j \leq k$ are eventually constant along the sequence.

Second, a sequence indexed by $N$ is long enough to reach the limit. For each of the countably many thresholds $t^{- k}$ there is an index $N_{k}$ past which the sequence is that close, and $\sup$ -free bookkeeping over $N$ assembles the $N_{k}$ into a single limit. In a field whose value group had uncountable cofinality this last step would fail, and a sequence would not suffice.

The one genuinely non-formal point is that the assembled $L$ must have support bounded below, so that it is an element of $K$ at all. That does not follow from the eventual constancy at each index separately; it comes from the single threshold $k = 0$ , which already pins down every negative index at once.

Facts & Assumptions

Given: A sequence $(f^{(n)})_{n \in N}$ in $K$ that is Cauchy in $K$ .

[L1]

$K$ consists of the functions $Z \to R$ whose support is bounded below; $t^{- a}$ is $1$ at index $a$ and $0$ elsewhere (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$K$ is an ordered field, so its order is transitive and total ( $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient, Ordered field, Absolute value in an ordered field); and $(g - h) (j) = g (j) - h (j)$ for $g, h \in K$ ( $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below).

[L3]

In $K$ : $0_{K} < t^{- (k + 1)} < t^{- k}$ for every $k \in Z$ ; for every $ε > 0$ in $K$ there is $k \in N$ with $t^{- k} < ε$ ; if $h (j) = 0$ for every $j \leq k$ then $∣ h ∣ < t^{- k}$ ; and if $∣ h ∣ < t^{- k}$ then $h (j) = 0$ for every $j < k$ ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements).

[L4]

$(x_{n})$ is Cauchy in $K$ when for every $ε > 0$ in $K$ there is $N \in N$ with $∣ x_{n} - x_{m} ∣ < ε$ for all $n, m \geq N$ ; and $(x_{n})$ converges to $L$ in $K$ when for every $ε > 0$ in $K$ there is $N$ with $∣ x_{n} - L ∣ < ε$ for all $n \geq N$ (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L5]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L6]

The order on $N$ is total ( $\leq$ is a linear order on $N$ , Order on the natural numbers), induction is available (The principle of mathematical induction, The natural numbers $N$ (von Neumann)), and every integer $\geq 0$ is the image of a unique natural number, so a natural number may be used as an index in $Z$ (The naturals embed in the integers).

Proof

technique · constructive

1.1

For $k \in N$ put $M_{k} : = {N \in N : ∣ f^{(n)} - f^{(m)} ∣ < t^{- (k + 1)} for all n, m \geq N}$ . Since $t^{- (k + 1)} > 0_{K}$ by [L3] and the sequence is Cauchy, $M_{k} \neq \emptyset$ by [L4]; let $N_{k} : = \min M_{k}$ , which exists by [L5].

givenL3L4L5construct

2.1

For every $k \in N$ , all $n, m \geq N_{k}$ and every $j \leq k$ one has $f^{(n)} (j) = f^{(m)} (j)$ : by [step 1.1] $∣ f^{(n)} - f^{(m)} ∣ < t^{- (k + 1)}$ , so [L3] gives $(f^{(n)} - f^{(m)}) (j) = 0$ for every $j < k + 1$ , that is for every $j \leq k$ , and $(f^{(n)} - f^{(m)}) (j) = f^{(n)} (j) - f^{(m)} (j)$ by [L2].

step 1.1L2L3L6

2.2

$N_{a} \leq N_{b}$ whenever $a \leq b$ in $N$ : for consecutive indices, $t^{- (k + 2)} < t^{- (k + 1)}$ by [L3], so any $N$ witnessing membership in $M_{k + 1}$ also witnesses membership in $M_{k}$ by transitivity of the order [L2]; hence $M_{k + 1} \subseteq M_{k}$ and $N_{k} = \min M_{k} \leq \min M_{k + 1} = N_{k + 1}$ . The general case follows by induction on $b$ [L6].

step 1.1L2L3L6

2.3

Define $κ : Z \to N$ by $κ (j) : = j$ for $j \geq 0$ and $κ (j) : = 0$ for $j < 0$ , so that $j \leq κ (j)$ for every $j \in Z$ ; then define $L : Z \to R$ by $L (j) : = f^{(N_{κ (j)})} (j)$ .

step 1.1L6construct

3.1

For every $j \in Z$ and every $n \geq N_{κ (j)}$ one has $f^{(n)} (j) = L (j)$ : apply [step 2.1] with $k = κ (j)$ , which is legitimate since $j \leq κ (j)$ , to the two indices $n$ and $N_{κ (j)}$ , both of which are $\geq N_{κ (j)}$ .

step 2.1step 2.3L6

3.2

$L \in K$ . The series $f^{(N_{0})}$ lies in $K$ , so by [L1] there is $m_{0} \in Z$ with $f^{(N_{0})} (j) = 0$ for every $j < m_{0}$ . If $j < m_{0}$ and $j < 0$ then $κ (j) = 0$ , so $L (j) = f^{(N_{0})} (j) = 0$ ; hence $L (j) = 0$ for every $j$ below both $m_{0}$ and $0$ , the support of $L$ is bounded below, and $L \in K$ .

step 2.3L1

4.1

For every $k \in N$ , every $n \geq N_{k}$ and every $j \leq k$ one has $f^{(n)} (j) = L (j)$ : if $j \geq 0$ then $κ (j) = j \leq k$ , and if $j < 0$ then $κ (j) = 0 \leq k$ , so in both cases $N_{κ (j)} \leq N_{k} \leq n$ by [step 2.2] and [step 3.1] applies.

step 2.2step 3.1L6

5.1

$(f^{(n)})$ converges to $L$ in $K$ . Let $ε > 0$ in $K$ . By [L3] — this is the countable-cofinality step, and it is the only place where anything special about $K$ is used — there is $k \in N$ with $t^{- k} < ε$ . Put $N : = N_{k}$ . For every $n \geq N$ , [step 4.1] and [L2] give $(f^{(n)} - L) (j) = f^{(n)} (j) - L (j) = 0$ for every $j \leq k$ , so $∣ f^{(n)} - L ∣ < t^{- k}$ by [L3] and therefore $∣ f^{(n)} - L ∣ < ε$ by transitivity [L2]. As $ε$ was arbitrary, this is convergence in the sense of [L4].

step 3.2step 4.1L2L3L4

6.1

The sequence $(f^{(n)})$ was an arbitrary Cauchy sequence in $K$ , and [step 3.2] and [step 5.1] produce an element $L \in K$ to which it converges; so every Cauchy sequence in $K$ converges in $K$ .

step 3.2step 5.1discharge-construct∎

Remarks

What makes the argument work, in one sentence. The value group of $K$ is $Z$ , whose cofinality is countable, so the continuum of thresholds $ε > 0$ in the Cauchy condition collapses to the countable family $t^{- k}$ , $k \in N$ ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements, clause 3), and a sequence indexed by $N$ can meet all of them. A proof that skipped this step would be proving nothing: it is exactly the point at which the countability of the index set $N$ is matched to the structure of the field.
Support-boundedness of the limit is a separate obligation, and it is discharged from a single threshold. Knowing that each coefficient $f^{(n)} (j)$ is eventually constant gives a function $Z \to R$ and nothing more; there is no reason a priori why its support should be bounded below. What supplies that is [step 3.2]: the threshold $k = 0$ freezes all indices $j \leq 0$ simultaneously from the single stage $N_{0}$ onward, so $L$ agrees with the one series $f^{(N_{0})}$ on the whole negative half-line and inherits its lower bound.
No choice is used. The stage $N_{k}$ is not chosen: it is defined as the least element of $M_{k}$ , which exists by the well-ordering principle (The well-ordering principle). This matters because the construction makes countably many selections, and a version of it that said "pick some $N_{k}$ " would be an appeal to countable choice for no reason.
This is Cauchy completeness and nothing more. $K$ is sequentially Cauchy complete and at the same time lacks the least-upper-bound property ( $R ((t^{- 1}))$ does not have the least-upper-bound property; its canonical naturals have no supremum); the two are not the same condition, and in a non-Archimedean field they come apart. Nor does this theorem give the unrestricted nested interval property: see $R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$ for what it does give, and The unrestricted nested interval property fails in $R ((t^{- 1}))$ for what it does not.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-08 (gpt-5.6-terra-codex-subscription)Open item page →

$R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$

Statement

Let $K = R ((t^{- 1}))$ and let $(I_{n})_{n \in N}$ with $I_{n} = [a_{n}, b_{n}]_{K}$ be a nested sequence of closed intervals in $K$ whose lengths tend to $0$ in $K$ , that is, for every $ε > 0$ in $K$ there is $N$ with $b_{n} - a_{n} < ε$ for all $n \geq N$ (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field). Then

$⋂_{n \in N} I_{n}$

contains exactly one element of $K$ .

The hypothesis that the lengths tend to $0$ may not be dropped: this is the nested interval property in its shrinking form only, and nothing on this page establishes the unrestricted form for $K$ . The remarks below record what happens without the hypothesis.

Facts & Assumptions

Given: A nested sequence $(I_{n})_{n \in N}$ of closed intervals $I_{n} = [a_{n}, b_{n}]_{K}$ in $K$ , so $a_{n} \leq b_{n}$ and $I_{n + 1} \subseteq I_{n}$ for every $n$ , whose lengths tend to $0$ in $K$ .

[L1]

$[a, b]_{K} = {x \in K : a \leq x \leq b}$ for $a \leq b$ ; a sequence $(x_{n})$ in $K$ is Cauchy in $K$ when for every $ε > 0$ in $K$ there is $N$ with $∣ x_{n} - x_{m} ∣ < ε$ for all $n, m \geq N$ , and converges to $L$ when for every $ε > 0$ in $K$ there is $N$ with $∣ x_{n} - L ∣ < ε$ for all $n \geq N$ ; the lengths $b_{n} - a_{n}$ tend to $0$ when for every $ε > 0$ in $K$ they are eventually $< ε$ (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L2]

Every Cauchy sequence in $K$ converges in $K$ (Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete).

[L3]

$K$ is an ordered field ( $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient, Ordered field), so its order is total and transitive and $x < y$ means $0 < y - x$ . Compatibility with addition is used below in its NONSTRICT form, $x \leq y \Rightarrow x + z \leq y + z$ , whereas Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those ( $x < y \Rightarrow x + z < y + z$ , and $x < y$ with $z < w$ giving $x + z < y + w$ ); the nonstrict form is the first strict form together with the case $x = y$ , where the two sides are equal, the order being total (Ordered field).

[L4]

$∣ z ∣ \geq 0$ , $∣ z ∣ = 0$ only for $z = 0$ , and $∣ z ∣$ equals $z$ or $- z$ ; so $∣ z ∣ = z$ when $z \geq 0$ (Basic properties of the absolute value, Absolute value in an ordered field).

[L5]

The order on $N$ is total ( $\leq$ is a linear order on $N$ , Order on the natural numbers) and induction is available (The principle of mathematical induction, The natural numbers $N$ (von Neumann)).

Proof

technique · direct

1.1

For each $n$ , the endpoints $a_{n + 1}$ and $b_{n + 1}$ belong to $I_{n + 1}$ because $a_{n + 1} \leq b_{n + 1}$ , and $I_{n + 1} \subseteq I_{n}$ , so both belong to $I_{n}$ ; by [L1] this says $a_{n} \leq a_{n + 1}$ and $b_{n + 1} \leq b_{n}$ . Hence $a_{n} \leq a_{n + 1} \leq b_{n + 1} \leq b_{n}$ .

givenL1L3

1.2

The intersection contains at most one element. Suppose $x, y \in ⋂_{n} I_{n}$ with $x \neq y$ , so $∣ x - y ∣ > 0$ by [L4]. For each $n$ both $x$ and $y$ lie in $[a_{n}, b_{n}]_{K}$ , so $x - y \leq b_{n} - a_{n}$ and $y - x \leq b_{n} - a_{n}$ by [L1] and [L3], and since $∣ x - y ∣$ is one of $x - y$ , $y - x$ by [L4] we get $∣ x - y ∣ \leq b_{n} - a_{n}$ for every $n$ . Applying the shrinking hypothesis with $ε : = ∣ x - y ∣$ produces some $n$ with $b_{n} - a_{n} < ∣ x - y ∣$ , a contradiction.

givenL1L3L4

2.1

Whenever $n \leq m$ one has $a_{n} \leq a_{m} \leq b_{m} \leq b_{n}$ : this is [step 1.1] for $m = n + 1$ , it is trivial for $m = n$ , and the general case follows by induction on $m$ using transitivity of the order.

step 1.1L3L5

3.1

$(a_{n})_{n \in N}$ is Cauchy in $K$ . Let $ε > 0$ in $K$ and take $N$ with $b_{n} - a_{n} < ε$ for all $n \geq N$ . Let $n, m \geq N$ ; by [L5] we may assume $n \leq m$ , the other case being the same with the roles exchanged. By [step 2.1], $a_{n} \leq a_{m} \leq b_{m} \leq b_{n}$ , so $0 \leq a_{m} - a_{n} \leq b_{n} - a_{n} < ε$ , and $∣ a_{m} - a_{n} ∣ = a_{m} - a_{n} < ε$ by [L4].

step 2.1givenL1L3L4L5

4.1

By [L2] there is $L \in K$ with $a_{n} \to L$ in $K$ .

step 3.1L2

5.1

$a_{n} \leq L$ for every $n$ . Otherwise $L < a_{n}$ for some $n$ ; put $ε : = a_{n} - L > 0$ and use [step 4.1] to fix $N$ with $∣ a_{m} - L ∣ < ε$ for all $m \geq N$ . Pick $m$ with $m \geq N$ and $m \geq n$ ([L5]). By [step 2.1], $a_{n} \leq a_{m}$ , so $a_{m} - L \geq a_{n} - L = ε > 0$ and hence $∣ a_{m} - L ∣ = a_{m} - L \geq ε$ by [L4], contradicting $∣ a_{m} - L ∣ < ε$ .

step 2.1step 4.1L1L3L4L5

5.2

$L \leq b_{n}$ for every $n$ . Otherwise $b_{n} < L$ for some $n$ ; put $ε : = L - b_{n} > 0$ and fix $N$ with $∣ a_{m} - L ∣ < ε$ for all $m \geq N$ . Pick $m$ with $m \geq N$ and $m \geq n$ . By [step 2.1], $a_{m} \leq b_{m} \leq b_{n}$ , so $L - a_{m} \geq L - b_{n} = ε > 0$ and hence $∣ a_{m} - L ∣ = L - a_{m} \geq ε$ by [L4], again a contradiction.

step 2.1step 4.1L1L3L4L5

6.1

By [step 5.1] and [step 5.2], $a_{n} \leq L \leq b_{n}$ for every $n$ , so $L \in ⋂_{n} I_{n}$ by [L1] and the intersection is nonempty; by [step 1.2] it has no second element. Hence $⋂_{n} I_{n} = {L}$ .

step 5.1step 5.2step 1.2L1∎

Remarks

This is the shrinking form, and the restriction is real. The unrestricted nested interval property — every nested sequence of nonempty closed intervals meets — is false in $K$ , and The unrestricted nested interval property fails in $R ((t^{- 1}))$ exhibits a nested sequence with empty intersection. So the hypothesis here is not a convenience of the proof, and no item on this page may be cited for the unrestricted form.
A trap in the hypothesis: "lengths $2 / n$ " does not mean shrinking. The condition is that the lengths tend to $0$ in the order of $K$ , tested against every positive $ε \in K$ , not merely against positive real constants. A nested sequence whose $n$ -th length is the constant series $ι (2 / (n + 1))$ does not satisfy it: since $ι (c)$ takes the nonzero value $c$ at index $0$ , clause 4 of $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements forbids $∣ ι (c) ∣ < t^{- 1}$ , so no such length ever gets below $ε = t^{- 1}$ . Real-indexed shrinking is strictly weaker than shrinking in $K$ , and a proof that assumed the former would be proving a different theorem.
Where completeness enters. Exactly once, at [step 4.1]. Everything before it is monotonicity bookkeeping valid in any ordered field, and everything after it uses only the order and the absolute value. That is why the corollary is a corollary of Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete and not an independent argument about series.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

The unrestricted nested interval property fails in $R ((t^{- 1}))$

Statement refuted

Refuted claim: the unrestricted nested interval property holds in $K = R ((t^{- 1}))$ , that is, every nested sequence $I_{0} \supseteq I_{1} \supseteq \dots$ of closed intervals $I_{n} = [a_{n}, b_{n}]_{K}$ of $K$ (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field) has $⋂_{n} I_{n} \neq \emptyset$ .

The witness is

$a_{n} : = ι (n) t^{- 1}, b_{n} : = ι ⁣ (\frac{1}{n + 1}) (n \in N),$

where $ι (c)$ is the constant series with value $c$ at index $0$ and $ι (n)$ abbreviates $ι (n \cdot 1_{R})$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient). The intervals $[a_{n}, b_{n}]_{K}$ are nested and their intersection is empty: a common point would have to be an infinitesimal of valuation $\geq 1$ , because it lies below every positive real constant, and simultaneously not such an element, because it lies above every multiple $ι (n) t^{- 1}$ of $t^{- 1}$ .

This refutes only the unrestricted form. The shrinking form, with the additional hypothesis that the lengths tend to $0$ in $K$ , is true ( $R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$ ), and the lengths here do not tend to $0$ .

Facts & Assumptions

Given: $K = R ((t^{- 1}))$ with its valuation $v$ , leading coefficient $lc$ , monomials $t^{- a}$ and constants $ι (c)$ ; and the elements $a_{n} = ι (n) t^{- 1}$ , $b_{n} = ι (1 / (n + 1))$ for $n \in N$ .

[L1]

For nonzero $h \in K$ : $h (k) = 0$ for $k < v (h)$ and $h (v (h)) = lc (h) \neq 0$ ; $t^{- a}$ is nonzero with $v (t^{- a}) = a$ and $lc (t^{- a}) = 1$ ; and $ι (c)$ for $c \neq 0$ is nonzero with $v (ι (c)) = 0$ and $lc (ι (c)) = c$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient, $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient).

[L2]

$K$ is an ordered field in which $f < g$ holds exactly when $g - f \neq 0_{K}$ and $lc (g - f) > 0$ ; exactly one of $f < g$ , $f = g$ , $g < f$ holds; $ι$ is a ring homomorphism, so $ι (c) + ι (d) = ι (c + d)$ and $ι (c) ι (d) = ι (c d)$ ( $R ((t^{- 1}))$ is an ordered field, ordered by the sign of the leading coefficient, Ordered field).

[L3]

[L4]

$0_{K} < t^{- (k + 1)} < t^{- k}$ for every $k \in Z$ ; and if $∣ h ∣ < t^{- k}$ then $h (j) = 0$ for every $j < k$ ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements).

[L5]

$[a, b]_{K} = {x \in K : a \leq x \leq b}$ for $a \leq b$ ; a sequence of closed intervals is nested when $I_{n + 1} \subseteq I_{n}$ for every $n$ ; and its lengths tend to $0$ in $K$ when for every $ε > 0$ in $K$ they are eventually $< ε$ (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L6]

$R$ is a complete ordered field, hence Archimedean: for every real $c$ there is a natural $n$ with $c < n \cdot 1_{R}$ , and for every real $c > 0$ there is a natural $n \geq 1$ with $1 / n < c$ (The reals form a totally ordered field, The Cauchy-sequence reals have the least-upper-bound property, Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Counterexample

technique · direct

1.1

For $n \geq 1$ the element $a_{n} = ι (n) t^{- 1}$ is nonzero with $v (a_{n}) = 0 + 1 = 1$ and $lc (a_{n}) = n \cdot 1 = n > 0$ , while $a_{0} = ι (0) t^{- 1} = 0_{K}$ ; and for every $n$ the element $b_{n} = ι (1 / (n + 1))$ is nonzero with $v (b_{n}) = 0$ and $lc (b_{n}) = 1 / (n + 1) > 0$ . Also $a_{1} = ι (1) t^{- 1} = t^{- 1}$ .

givenL1L2L3

2.1

$a_{n} \leq b_{n}$ for every $n$ : for $n = 0$ this is $0_{K} < ι (1) = 1_{K}$ , which holds since $lc (1_{K}) = 1 > 0$ ; and for $n \geq 1$ we have $v (b_{n}) = 0 < 1 = v (- a_{n})$ by [step 1.1] and [L3], so $b_{n} - a_{n}$ is nonzero with leading coefficient $1 / (n + 1) > 0$ , that is $a_{n} < b_{n}$ . So each $[a_{n}, b_{n}]_{K}$ is a closed interval.

step 1.1L1L2L3L5

2.2

The sequence is nested: $a_{n + 1} - a_{n} = (ι (n + 1) - ι (n)) t^{- 1} = ι (1) t^{- 1} = t^{- 1} > 0_{K}$ by [L2] and [L4], so $a_{n} < a_{n + 1}$ ; and $b_{n} - b_{n + 1} = ι (\frac{1}{n + 1} - \frac{1}{n + 2}) = ι (\frac{1}{(n + 1) (n + 2)})$ , which is nonzero with positive leading coefficient, so $b_{n + 1} < b_{n}$ . Hence $a_{n} \leq a_{n + 1}$ and $b_{n + 1} \leq b_{n}$ , and every $x$ with $a_{n + 1} \leq x \leq b_{n + 1}$ satisfies $a_{n} \leq x \leq b_{n}$ , that is $I_{n + 1} \subseteq I_{n}$ .

step 1.1L1L2L3L4L5

3.1

Suppose $x \in ⋂_{n} I_{n}$ . Then $a_{1} \leq x$ , and $a_{1} = t^{- 1} > 0_{K}$ by [step 1.1] and [L4], so $x > 0_{K}$ ; hence $x \neq 0_{K}$ and $lc (x) > 0$ by [L2]. Write $q : = v (x)$ and $c : = lc (x) > 0$ .

step 1.1step 2.1L1L2L4L5

4.1

$q \geq 1$ . If $q < 0$ then $v (x) < 0 = v (- b_{0})$ by [step 1.1] and [L3], so $x - b_{0}$ is nonzero with leading coefficient $c > 0$ and $x > b_{0}$ , contradicting $x \leq b_{0}$ . If $q = 0$ , use [L6] to fix a natural $n \geq 1$ with $1 / n < c$ and set $n^{'} : = n - 1$ , so that $1 / (n^{'} + 1) < c$ ; then $x$ and $- b_{n^{'}}$ both have valuation $0$ with leading coefficients summing to $c - 1 / (n^{'} + 1) \neq 0$ , so by [L3] $x - b_{n^{'}}$ is nonzero with leading coefficient $c - 1 / (n^{'} + 1) > 0$ , giving $x > b_{n^{'}}$ and contradicting $x \leq b_{n^{'}}$ . By trichotomy on $Z$ the remaining case is $q \geq 1$ .

step 3.1L1L2L3L5L6

4.2

$q < 1$ . If $q > 1$ then $v (- a_{1}) = 1 < q$ by [step 1.1] and [L3], so $x - a_{1}$ is nonzero with leading coefficient $lc (- a_{1}) = - 1 < 0$ , giving $x < a_{1}$ and contradicting $a_{1} \leq x$ . If $q = 1$ , use [L6] to fix a natural $n$ with $c < n \cdot 1_{R}$ , so $n \geq 1$ ; then $x$ and $- a_{n}$ both have valuation $1$ with leading coefficients summing to $c - n \neq 0$ , so by [L3] $x - a_{n}$ is nonzero with leading coefficient $c - n < 0$ , giving $x < a_{n}$ and contradicting $a_{n} \leq x$ . Hence $q \neq 1$ and $q ≯ 1$ .

step 3.1L1L2L3L5L6

5.1

Steps 4.1 and 4.2 are incompatible, so no $x$ lies in every $I_{n}$ : the nested sequence $(I_{n})$ of [step 2.1] and [step 2.2] has $⋂_{n} I_{n} = \emptyset$ , which refutes the unrestricted nested interval property for $K$ .

step 2.1step 2.2step 4.1step 4.2L5

6.1

Consistency with $R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$ : the lengths here do not tend to $0$ in $K$ . Indeed $(b_{n} - a_{n}) (0) = 1 / (n + 1) \neq 0$ by [step 1.1], so by [L4] the inequality $∣ b_{n} - a_{n} ∣ < t^{- 1}$ fails for every $n$ ; taking $ε = t^{- 1}$ shows the shrinking hypothesis of [L5] is not satisfied.

step 1.1step 2.1L4L5∎

Remarks

What the counterexample really exhibits. It is a gap in $K$ . Each of the two requirements is satisfiable on its own — $ι (1)$ lies above every $ι (n) t^{- 1}$ , and $0_{K}$ lies below every $ι (1 / (n + 1))$ — yet steps 4.1 and 4.2 show that nothing in $K$ satisfies both at once. Both sides of the gap are approached along countable sequences, which is why intervals indexed by $N$ can straddle it, and the lengths cannot shrink across it: they stay of valuation $0$ while the left endpoints stay of valuation $1$ .
Why this does not contradict Cauchy completeness. $(a_{n})$ is not Cauchy in $K$ : consecutive terms differ by exactly $t^{- 1}$ , so the Cauchy condition fails at $ε = t^{- 1}$ . Cauchy completeness (Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete) constrains sequences whose terms crowd together in the order of $K$ , and neither endpoint sequence here does.
Consequence for the equivalence of completeness properties. Since $K$ is Cauchy complete but has neither the least-upper-bound property ( $R ((t^{- 1}))$ does not have the least-upper-bound property; its canonical naturals have no supremum) nor the unrestricted nested interval property, any statement of the form "nested intervals imply least upper bounds" has to say which nested interval property it means. The form that $K$ does satisfy is the shrinking one, and that is the form for which $K$ is a counterexample to the implication.

The Formal Laurent Series Field R((t−1))R((t−1)): Cauchy Complete, Non-Archimedean, Not Complete

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The formal Laurent series R((t−1))R((t−1)): support bounded below, valuation, leading coefficient

Definition

Remarks

R((t−1))R((t−1)) is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Statement

Facts & Assumptions

Proof

Valuation and leading coefficient in R((t−1))R((t−1)): v(fg)=v(f)+v(g)v(fg)=v(f)+v(g), and the behaviour of vv under sums

Statement

Facts & Assumptions

Proof

R((t−1))R((t−1)) is a field: every nonzero formal Laurent series is invertible

Statement

Facts & Assumptions

Proof

Remarks

R((t−1))R((t−1)) is an ordered field, ordered by the sign of the leading coefficient

Statement

Facts & Assumptions

Proof

Remarks

R((t−1))R((t−1)) is non-Archimedean, and the monomials t−kt−k are cofinal below its positive elements

Statement

Facts & Assumptions

Proof

Remarks

R((t−1))R((t−1)) does not have the least-upper-bound property; its canonical naturals have no supremum

Statement

Facts & Assumptions

Proof

Remarks

Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field

Definition

Remarks

Every Cauchy sequence in R((t−1))R((t−1)) converges: KK is sequentially Cauchy complete

Statement

Facts & Assumptions

Proof

Remarks

R((t−1))R((t−1)) has the nested interval property for lengths tending to 00

Statement

Facts & Assumptions

Proof

Remarks

5 · Examples, counterexamples and false statements

The unrestricted nested interval property fails in R((t−1))R((t−1))

Statement refuted

Facts & Assumptions

Counterexample

Remarks

Sources

The Formal Laurent Series Field $R ((t^{- 1}))$ : Cauchy Complete, Non-Archimedean, Not Complete

The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient

$R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums

$R ((t^{- 1}))$ is a field: every nonzero formal Laurent series is invertible

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

$R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements

$R ((t^{- 1}))$ does not have the least-upper-bound property; its canonical naturals have no supremum

Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete

$R ((t^{- 1}))$ has the nested interval property for lengths tending to $0$

The unrestricted nested interval property fails in $R ((t^{- 1}))$