Alphabeta Math
Session-authored (Fable 5 assisted)
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((t1))\mathbb{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((t1))K = \mathbb{R}((t^{-1})), the formal Laurent series in t1t^{-1} over R\mathbb{R}, and what is proved here is that KK 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)\mathbb{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)\mathbb{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)\mathbb{R}(t) and does not need to. KK 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 KK is an arbitrary series in descending powers of tt rather than a ratio of polynomials. This page does not construct an embedding of R(t)\mathbb{R}(t) into KK and never uses one; the relationship is recorded honestly in the remarks of The formal Laurent series R((t1))\mathbb{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((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient defines an element of KK as a function ZR\mathbb{Z} \to \mathbb{R} whose support is bounded below, written kk0aktk\sum_{k \ge k_0} a_k t^{-k}, with the valuation v(f)v(f) its lowest nonzero index and lc(f)\operatorname{lc}(f) the coefficient there. R((t1))\mathbb{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((t1))\mathbb{R}((t^{-1})): v(fg)=v(f)+v(g)v(fg) = v(f) + v(g), and the behaviour of vv under sums then records the two facts that every later argument runs on, v(fg)=v(f)+v(g)v(fg) = v(f) + v(g) and the behaviour of vv under sums, from which KK is at once an integral domain.

The genuinely non-trivial algebra is R((t1))\mathbb{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 KK has no notion of an infinite sum. What replaces it is the observation that unu^{n} vanishes at every index below nn when uu does below 11, 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\mathbb{R}. R((t1))\mathbb{R}((t^{-1})) is an ordered field, ordered by the sign of the leading coefficient orders KK by the sign of the leading coefficient: f>0f > 0 exactly when the lowest-index nonzero coefficient of ff 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 KK. R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements draws the consequences: tt exceeds every canonical natural, so KK is not Archimedean; the monomials tkt^{-k} decrease; and, the clause that matters most, every positive element of KK exceeds some tkt^{-k} with kNk \in \mathbb{N}. The value group is Z\mathbb{Z}, whose cofinality is countable, and that clause is what countable cofinality means down in the order.

R((t1))\mathbb{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, KK is not, so KK is not complete. The concrete route names the set that fails, the canonical naturals {n1K}\{n \cdot 1_K\}, which are bounded above by tt 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 KK is Cauchy complete is entitled to see precisely which set has no supremum.

Sequences in a field that is not R\mathbb{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 FF, 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 ε\varepsilon range over FF, 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 KK. And a theorem proved about sequences of reals is a theorem about R\mathbb{R}; it may not be cited for a general FF merely because its proof looks like it would transfer.

Cauchy completeness, and why the argument is not a formality. Every Cauchy sequence in R((t1))\mathbb{R}((t^{-1})) converges: KK is sequentially Cauchy complete is the main theorem. Its hinge is the countable-cofinality clause of R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements: the continuum of thresholds in the Cauchy condition collapses to the countable family tkt^{-k}, so testing against those suffices, and a sequence indexed by N\mathbb{N} is long enough to meet all of them. Applying the condition at t(k+1)t^{-(k+1)} says that the coefficients at all indices jkj \le 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=0k = 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((t1))\mathbb{R}((t^{-1})) has the nested interval property for lengths tending to 00 deduces from Cauchy completeness that a nested sequence of closed intervals whose lengths tend to 00 in the order of KK meets in exactly one point. The restriction is not a weakness of the proof. The unrestricted property is false in KK, and The unrestricted nested interval property fails in R((t1))\mathbb{R}((t^{-1})) exhibits nested intervals [ι(n)t1,ι(1/(n+1))][\iota(n)t^{-1},\, \iota(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 t1t^{-1}, which no element of KK is. The shrinking hypothesis must also be read in KK and not in R\mathbb{R}, and both items say so. The lengths in the counterexample keep a nonzero coefficient at index 00, so not one of them ever gets below t1t^{-1}; and the remarks of R((t1))\mathbb{R}((t^{-1})) has the nested interval property for lengths tending to 00 make the same point with lengths that are the real constants 2/(n+1)2/(n+1), which tend to 00 in the ordinary real sense and do not tend to 00 in KK 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 KK, 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((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient

Definition

Throughout, R\mathbb{R} is the field of real numbers with its order (The real numbers, The reals form a totally ordered field) and Z\mathbb{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:ZRf : \mathbb{Z} \to \mathbb{R} write

suppf  :=  {kZ:f(k)0},\operatorname{supp} f \;:=\; \{\, k \in \mathbb{Z} : f(k) \ne 0 \,\},

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

K  =  R((t1))  :=  {f:ZR    suppf is bounded below},K \;=\; \mathbb{R}((t^{-1})) \;:=\; \{\, f : \mathbb{Z} \to \mathbb{R} \;\mid\; \operatorname{supp} f \text{ is bounded below} \,\},

equipped with

(f+g)(k):=f(k)+g(k),(fg)(k):=i+j=kf(i)g(j),(f + g)(k) := f(k) + g(k), \qquad (fg)(k) := \sum_{i + j = k} f(i)\,g(j),

where the product sum ranges over the pairs (i,j)Z×Z(i,j) \in \mathbb{Z} \times \mathbb{Z} with i+j=ki + j = k and f(i)g(j)0f(i)g(j) \ne 0. That set of pairs is finite for every kk, and f+gf + g and fgfg again lie in KK: this is R((t1))\mathbb{R}((t^{-1})) is a commutative ring: the product is a finite sum and both operations preserve support bounded below , which also proves that KK with these operations is a commutative ring whose zero 0K0_K is the constant function 00 and whose identity 1K1_K is the function taking the value 11 at 00 and 00 elsewhere.

Distinguished elements. For nZn \in \mathbb{Z} let tnKt^{-n} \in K be the function taking the value 11 at nn and 00 at every other index; so t0=1Kt^{0} = 1_K, and t:=t(1)t := t^{-(-1)} is the function taking the value 11 at 1-1. For cRc \in \mathbb{R} let ι(c)K\iota(c) \in K be the function taking the value cc at 00 and 00 elsewhere. The notation tnt^{-n} is defined here as a name; that it is consistent with the ring multiplication, tmtn=t(m+n)t^{-m} \, t^{-n} = t^{-(m+n)}, is proved in R((t1))\mathbb{R}((t^{-1})) is a commutative ring: the product is a finite sum and both operations preserve support bounded below .

Series notation. Because suppf\operatorname{supp} f is bounded below, say by mm, one writes

f  =  kmf(k)tk,f \;=\; \sum_{k \ge m} f(k)\, t^{-k},

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

Valuation and leading coefficient. Let fKf \in K with f0Kf \ne 0_K. Then suppf\operatorname{supp} f is nonempty and bounded below, so it has a least element (R((t1))\mathbb{R}((t^{-1})) is a commutative ring: the product is a finite sum and both operations preserve support bounded below ). Define

v(f)  :=  minsuppfZ,lc(f)  :=  f(v(f))R{0}.v(f) \;:=\; \min \operatorname{supp} f \in \mathbb{Z}, \qquad \operatorname{lc}(f) \;:=\; f(v(f)) \in \mathbb{R} \setminus \{0\}.

v(f)v(f) is the valuation and lc(f)\operatorname{lc}(f) the leading coefficient of ff. Neither is defined at f=0Kf = 0_K, whose support is empty; every statement about vv or lc\operatorname{lc} in this library carries the hypothesis f0Kf \ne 0_K explicitly.

Order. The positive cone of KK is

P  :=  {fK:f0K and lc(f)>0},P \;:=\; \{\, f \in K : f \ne 0_K \text{ and } \operatorname{lc}(f) > 0 \,\},

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

Remarks

  • Why the support must be bounded below. It is exactly what makes the product a finite sum. If arbitrary functions ZR\mathbb{Z} \to \mathbb{R} were admitted, the defining sum for (fg)(k)(fg)(k) would range over an infinite set of pairs and would denote nothing, since KK carries no notion of convergence. The condition is preserved by both operations, which is the content of R((t1))\mathbb{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\mathbb{Z}, and the edge cases are real. The zero series has empty support and no valuation. A nonzero constant series ι(c)\iota(c) has v(ι(c))=0v(\iota(c)) = 0 and lc(ι(c))=c\operatorname{lc}(\iota(c)) = c, so the index k=0k = 0 is an ordinary index and not a boundary. Negative indices are admitted, and they are what makes t=t(1)t = t^{-(-1)}, whose support is {1}\{-1\}, an element of KK; 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 t1t^{-1} smaller than every positive real constant while tt is larger than every real constant. The consequences are drawn in R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements.

  • Relation to the rational functions. The ordered field R(t)\mathbb{R}(t) of Not every ordered field is Archimedean, ordered so that f>0f > 0 exactly when f(x)>0f(x) > 0 for all sufficiently large real xx, is the standard first example of a non-Archimedean ordered field, and standard treatments identify it with a subfield of KK 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 KK 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((t1))\mathbb{R}((t^{-1})) is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Statement

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

  1. (Finiteness.) For every kZk \in \mathbb{Z} the set Sk:={(i,j)Z×Z:i+j=k,  f(i)g(j)0}S_k := \{\, (i,j) \in \mathbb{Z} \times \mathbb{Z} : i + j = k,\; f(i)g(j) \ne 0 \,\} is finite, so (fg)(k)=i+j=kf(i)g(j)(fg)(k) = \sum_{i+j=k} f(i)g(j) is a finite sum of reals; and Sk=S_k = \varnothing whenever k<m+nk < m + n.
  2. (Closure.) f+gf + g, f-f and fgfg lie in KK, with (f+g)(k)=0(f+g)(k) = 0 for k<min(m,n)k < \min(m,n) and (fg)(k)=0(fg)(k) = 0 for k<m+nk < m + n.
  3. (Ring.) (K,+,,0K,1K)(K, +, \cdot\,, 0_K, 1_K) is a commutative ring with identity, and 1K0K1_K \ne 0_K.
  4. (Monomials and constants.) (tah)(k)=h(ka)(t^{-a}h)(k) = h(k-a) for every hKh \in K and all a,kZa, k \in \mathbb{Z}; consequently tatb=t(a+b)t^{-a} \, t^{-b} = t^{-(a+b)} for all a,bZa, b \in \mathbb{Z}. Moreover (ι(c)f)(k)=cf(k)(\iota(c)f)(k) = c\, f(k) for all cRc \in \mathbb{R} and kZk \in \mathbb{Z}.
  5. (Least element.) Every nonempty SZS \subseteq \mathbb{Z} that is bounded below has a least element. In particular suppf\operatorname{supp} f has a least element whenever f0Kf \ne 0_K, so the valuation v(f)v(f) and the leading coefficient lc(f)\operatorname{lc}(f) of The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient are defined.

Facts & Assumptions

Given: KK, its operations, 0K0_K, 1K1_K, the monomials tnt^{-n} and the constants ι(c)\iota(c) as in The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient; elements f,gKf, g \in K and bounds m,nZm, n \in \mathbb{Z} with f(i)=0f(i) = 0 for i<mi < m and g(j)=0g(j) = 0 for j<nj < n.

[L1]

KK consists of the functions ZR\mathbb{Z} \to \mathbb{R} whose support is bounded below; (f+g)(k)=f(k)+g(k)(f+g)(k) = f(k) + g(k) and (fg)(k)=i+j=kf(i)g(j)(fg)(k) = \sum_{i+j=k} f(i)g(j); 0K0_K is the zero function, 1K1_K is 11 at index 00 and 00 elsewhere, tat^{-a} is 11 at index aa and 00 elsewhere, and ι(c)\iota(c) is cc at index 00 and 00 elsewhere (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient).

[L2]

Z\mathbb{Z} is a totally ordered commutative ring: its order is total, and xyx \le y implies x+zy+zx + z \le y + z (The integers form a totally ordered ring, Order on the integers, Arithmetic on the integers).

[L3]

Every nonempty subset of N\mathbb{N} has a least element (The well-ordering principle).

[L4]

The map ε(a)=[(a,0)]\varepsilon(a) = [(a,0)] is injective from N\mathbb{N} onto the set of nonnegative integers and preserves addition and order, so every integer x0x \ge 0 is ε(a)\varepsilon(a) for a unique natural aa (The naturals embed in the integers).

[L5]

R\mathbb{R} is a field: addition and multiplication are associative and commutative, multiplication distributes over addition, 010 \ne 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 SZS \subseteq \mathbb{Z} be nonempty with sbs \ge b for all sSs \in S. Every element of T:={sb:sS}T := \{\, s - b : s \in S \,\} is a nonnegative integer, so by [L4] T={ε(a):aA}T = \{\, \varepsilon(a) : a \in A \,\} for a nonempty ANA \subseteq \mathbb{N}; by [L3] AA has a least element a0a_0, and since ε\varepsilon preserves order and xx+bx \mapsto x + b preserves order, ε(a0)+b\varepsilon(a_0) + b is an element of SS that is \le every element of SS.

L2L3L4
1.2

Fix kZk \in \mathbb{Z} and let (i,j)Sk(i,j) \in S_k. Then f(i)0f(i) \ne 0 and g(j)0g(j) \ne 0, so imi \ge m and jnj \ge n; from i+j=ki + j = k and jnj \ge n we get i=kjkni = k - j \le k - n. Hence miknm \le i \le k - n, and j=kij = k - i is determined by ii.

givenL1L2
2.1

The integers ii with miknm \le i \le k - n are in order-preserving bijection with the naturals aa satisfying ε(a)knm\varepsilon(a) \le k - n - m by [L4], and there are finitely many of these, none at all when knm<0k - n - m < 0; so SkS_k is a finite set by [step 1.2], it is empty whenever k<m+nk < m + n, and therefore (fg)(k)(fg)(k) is a finite sum of reals which is 00 whenever k<m+nk < m + n.

step 1.2L2L4L5
3.1

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

step 2.1givenL1L5
3.2

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

step 2.1L5
3.3

For f,g,hKf, g, h \in K and kZk \in \mathbb{Z}, expanding both ((fg)h)(k)((fg)h)(k) and (f(gh))(k)(f(gh))(k) by [L1] and [L5] gives the sum of f(i)g(j)h(l)f(i)g(j)h(l) over the triples (i,j,l)(i,j,l) with i+j+l=ki + j + l = k and f(i)g(j)h(l)0f(i)g(j)h(l) \ne 0; that set is finite because the argument of [step 1.2] bounds ii, jj and ll from below and hence, as in [step 2.1], from above as well. So multiplication on KK is associative.

step 1.2step 2.1L5
3.4

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

step 2.1L5
3.5

For hKh \in K, (tah)(k)=i+j=kta(i)h(j)(t^{-a}h)(k) = \sum_{i+j=k} t^{-a}(i)h(j) has at most one nonzero term, the one with i=ai = a and j=kaj = k - a, so (tah)(k)=h(ka)(t^{-a}h)(k) = h(k-a); taking h=tbh = t^{-b} gives (tatb)(k)=tb(ka)(t^{-a}t^{-b})(k) = t^{-b}(k-a), which is 11 when k=a+bk = a+b and 00 otherwise, that is, tatb=t(a+b)t^{-a}t^{-b} = t^{-(a+b)}.

step 2.1L1
3.6

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

step 2.1L1
3.7

(f1K)(k)=i+j=kf(i)1K(j)(f \cdot 1_K)(k) = \sum_{i+j=k} f(i) 1_K(j) has at most one nonzero term, the one with j=0j = 0 and i=ki = k, so (f1K)(k)=f(k)(f \cdot 1_K)(k) = f(k) and f1K=ff \cdot 1_K = f; moreover 1K(0)=10=0K(0)1_K(0) = 1 \ne 0 = 0_K(0), so 1K0K1_K \ne 0_K.

step 2.1L1L5
4.1

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

step 3.1L1L5
5.1

By [step 4.1] addition makes KK an abelian group, by [step 3.2], [step 3.3] and [step 3.7] multiplication is commutative and associative with identity 1K0K1_K \ne 0_K, and by [step 3.4] it distributes over addition; hence KK 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=suppfS = \operatorname{supp} f, which is nonempty when f0Kf \ne 0_K and bounded below because fKf \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((t1))\mathbb{R}((t^{-1})): v(fg)=v(f)+v(g)v(fg) = v(f) + v(g), and the behaviour of vv under sums

Statement

Let K=R((t1))K = \mathbb{R}((t^{-1})) with its valuation vv and leading coefficient lc\operatorname{lc} (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient), and let f,gKf, g \in K with f0Kf \ne 0_K and g0Kg \ne 0_K. Then:

  1. (Products.) fg0Kfg \ne 0_K, and v(fg)=v(f)+v(g),lc(fg)=lc(f)lc(g).v(fg) = v(f) + v(g), \qquad \operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g). In particular KK has no zero divisors.
  2. (Negatives.) f0K-f \ne 0_K, v(f)=v(f)v(-f) = v(f) and lc(f)=lc(f)\operatorname{lc}(-f) = -\operatorname{lc}(f).
  3. (Unequal valuations.) If v(f)<v(g)v(f) < v(g) then f+g0Kf + g \ne 0_K, v(f+g)=v(f)v(f+g) = v(f) and lc(f+g)=lc(f)\operatorname{lc}(f+g) = \operatorname{lc}(f).
  4. (Equal valuations, no cancellation.) If v(f)=v(g)=qv(f) = v(g) = q and lc(f)+lc(g)0\operatorname{lc}(f) + \operatorname{lc}(g) \ne 0, then f+g0Kf + g \ne 0_K, v(f+g)=qv(f+g) = q and lc(f+g)=lc(f)+lc(g)\operatorname{lc}(f+g) = \operatorname{lc}(f) + \operatorname{lc}(g).
  5. (Sums in general.) If f+g0Kf + g \ne 0_K then v(f+g)min{v(f),v(g)}v(f+g) \ge \min\{v(f), v(g)\}.

Facts & Assumptions

Given: f,gKf, g \in K with f0Kf \ne 0_K and g0Kg \ne 0_K; write p:=v(f)p := v(f) and q:=v(g)q := v(g).

[L1]

For a nonzero hKh \in K one has h(k)=0h(k) = 0 for every k<v(h)k < v(h) and h(v(h))=lc(h)0h(v(h)) = \operatorname{lc}(h) \ne 0; conversely, if h(k)=0h(k) = 0 for all k<rk < r and h(r)0h(r) \ne 0 then h0Kh \ne 0_K, v(h)=rv(h) = r and lc(h)=h(r)\operatorname{lc}(h) = h(r) (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient).

[L2]

(f+g)(k)=f(k)+g(k)(f+g)(k) = f(k) + g(k) and (fg)(k)=i+j=kf(i)g(j)(fg)(k) = \sum_{i+j=k} f(i)g(j), a finite sum; if ff vanishes at every index below mm and gg at every index below nn, then fgfg vanishes at every index below m+nm+n (R((t1))\mathbb{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((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient).

[L3]

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

[L4]

The order on Z\mathbb{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] ff vanishes at every index below pp and gg at every index below qq, so by [L2] (fg)(k)=0(fg)(k) = 0 for every k<p+qk < p + q.

L1L2
1.2

If (i,j)(i,j) satisfies i+j=p+qi + j = p+q and f(i)g(j)0f(i)g(j) \ne 0 then ipi \ge p and jqj \ge q by [L1], and i+j=p+qi + j = p + q then forces i=pi = p and j=qj = q; hence (fg)(p+q)=f(p)g(q)=lc(f)lc(g)(fg)(p+q) = f(p)g(q) = \operatorname{lc}(f)\operatorname{lc}(g), which is nonzero by [L3].

L1L2L3L4
1.3

(f)(k)=f(k)(-f)(k) = -f(k) for every kk, so f-f vanishes exactly where ff does; by [L1] and [L3] this gives f0K-f \ne 0_K, v(f)=pv(-f) = p and lc(f)=lc(f)0\operatorname{lc}(-f) = -\operatorname{lc}(f) \ne 0.

L1L2L3
1.4

Suppose p<qp < q. For k<pk < p both f(k)=0f(k) = 0 and g(k)=0g(k) = 0, so (f+g)(k)=0(f+g)(k) = 0; and g(p)=0g(p) = 0 because p<qp < q, so (f+g)(p)=lc(f)0(f+g)(p) = \operatorname{lc}(f) \ne 0. By [L1], f+g0Kf + g \ne 0_K with v(f+g)=pv(f+g) = p and lc(f+g)=lc(f)\operatorname{lc}(f+g) = \operatorname{lc}(f).

L1L2L4
1.5

Suppose p=qp = q and lc(f)+lc(g)0\operatorname{lc}(f) + \operatorname{lc}(g) \ne 0. For k<pk < p both terms vanish, so (f+g)(k)=0(f+g)(k) = 0; and (f+g)(p)=lc(f)+lc(g)0(f+g)(p) = \operatorname{lc}(f) + \operatorname{lc}(g) \ne 0. By [L1], f+g0Kf+g \ne 0_K, v(f+g)=pv(f+g) = p and lc(f+g)=lc(f)+lc(g)\operatorname{lc}(f+g) = \operatorname{lc}(f) + \operatorname{lc}(g).

L1L2
1.6

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

L1L2L4
2.1

By [step 1.1] fgfg vanishes at every index below p+qp+q and by [step 1.2] it is nonzero at p+qp+q; so by [L1] fg0Kfg \ne 0_K, v(fg)=p+qv(fg) = p + q and lc(fg)=lc(f)lc(g)\operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g). Since ff and gg were arbitrary nonzero elements, no product of nonzero elements of KK 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((t1))\mathbb{R}((t^{-1})) is a field: every nonzero formal Laurent series is invertible

Statement

K=R((t1))K = \mathbb{R}((t^{-1})) (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient) is a field (Field): it is a commutative ring with 1K0K1_K \ne 0_K, and every fKf \in K with f0Kf \ne 0_K has a multiplicative inverse in KK.

Explicitly, if p=v(f)p = v(f) and c=lc(f)c = \operatorname{lc}(f), then f=ι(c)tp(1Ku)f = \iota(c)\, t^{-p}\,(1_K - u) for the element uKu \in K given by u(j)=c1f(p+j)u(j) = -c^{-1}f(p+j) for j1j \ge 1 and u(j)=0u(j) = 0 for j0j \le 0, and f1=ι(c1)tpgf^{-1} = \iota(c^{-1})\, t^{p}\, g, where gKg \in K vanishes at every index <0< 0 and is given at k0k \ge 0 by g(k)=n=0k(un)(k)g(k) = \sum_{n=0}^{k} (u^{n})(k).

Scratch work

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

Facts & Assumptions

Given: A nonzero fKf \in K; write p:=v(f)Zp := v(f) \in \mathbb{Z} and c:=lc(f)R{0}c := \operatorname{lc}(f) \in \mathbb{R} \setminus \{0\}, so that f(k)=0f(k) = 0 for every k<pk < p and f(p)=cf(p) = c.

[L1]

KK is the set of functions ZR\mathbb{Z} \to \mathbb{R} whose support is bounded below; tat^{-a} is 11 at index aa and 00 elsewhere; ι(c)\iota(c) is cc at index 00 and 00 elsewhere; for nonzero hKh \in K one has h(k)=0h(k) = 0 for k<v(h)k < v(h) and h(v(h))=lc(h)0h(v(h)) = \operatorname{lc}(h) \ne 0 (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient).

[L2]

KK is a commutative ring with identity 1K0K1_K \ne 0_K; (h1h2)(k)=i+j=kh1(i)h2(j)(h_1h_2)(k) = \sum_{i+j=k} h_1(i)h_2(j) is a finite sum; if h1h_1 vanishes at every index <a< a and h2h_2 at every index <b< b then h1h2h_1h_2 vanishes at every index <a+b< a + b; (tah)(k)=h(ka)(t^{-a}h)(k) = h(k-a) and hence tatb=t(a+b)t^{-a}t^{-b} = t^{-(a+b)}; and (ι(c)h)(k)=ch(k)(\iota(c)h)(k) = c\,h(k) (R((t1))\mathbb{R}((t^{-1})) is a commutative ring: the product is a finite sum and both operations preserve support bounded below).

[L4]

R\mathbb{R} is a field: every nonzero cc has an inverse c1c^{-1} with cc1=1cc^{-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\mathbb{N}: for a set AA, an element aAa \in A and a function F:AAF : A \to A there is a unique Γ:NA\Gamma : \mathbb{N} \to A with Γ(0)=a\Gamma(0) = a and Γ(σ(n))=F(Γ(n))\Gamma(\sigma(n)) = F(\Gamma(n)) (The recursion theorem, The natural numbers N\mathbb{N} (von Neumann)).

[L6]

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

[L7]

A field is a commutative ring with 010 \ne 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:ZRu : \mathbb{Z} \to \mathbb{R} by u(j):=c1f(p+j)u(j) := -c^{-1} f(p + j) for j1j \ge 1 and u(j):=0u(j) := 0 for j0j \le 0. Then uu vanishes at every index <1< 1, so its support is bounded below and uKu \in K.

givenL1L4construct
1.2

By [L5] with A=KA = K, a=1Ka = 1_K and F(h)=huF(h) = hu there is a family (un)nN(u^{n})_{n \in \mathbb{N}} in KK with u0=1Ku^{0} = 1_K and uσ(n)=unuu^{\sigma(n)} = u^{n} u.

L2L5construct
2.1

For every kZk \in \mathbb{Z}, (ι(c)tp(1Ku))(k)=c(1Ku)(kp)\bigl(\iota(c)\,t^{-p}\,(1_K - u)\bigr)(k) = c\,(1_K - u)(k - p) by [L2]; this is 00 when k<pk < p because 1Ku1_K - u vanishes at every negative index, it is cc when k=pk = p, and it is c(u(kp))=cc1f(k)=f(k)c \cdot \bigl(-u(k-p)\bigr) = c c^{-1} f(k) = f(k) when k>pk > p. Comparing with f(k)=0f(k) = 0 for k<pk < p and f(p)=cf(p) = c, we get f=ι(c)tp(1Ku)f = \iota(c)\, t^{-p}\,(1_K - u).

step 1.1givenL1L2L4
2.2

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

step 1.1step 1.2L1L2L6
3.1

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

step 2.2L1L4construct
4.1

Fix k1k \ge 1. In (ug)(k)=i+j=ku(i)g(j)(ug)(k) = \sum_{i+j=k} u(i)g(j) a term can be nonzero only when i1i \ge 1 and j0j \ge 0, hence only for 1ik1 \le i \le k and j=kij = k - i; so (ug)(k)=i=1ku(i)g(ki)=i=1ku(i)n=0ki(un)(ki)(ug)(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 k0k \le 0 one has (ug)(k)=0(ug)(k) = 0, since uu vanishes at every index <1< 1 and gg at every index <0< 0, so every pair (i,j)(i,j) with i+j=ki + j = k has u(i)g(j)=0u(i)g(j) = 0.

step 1.1step 3.1L1L2
5.1

In the inner sum of [step 4.1] the terms with ki<nk1k - i < n \le k-1 vanish by [step 2.2], so the inner sum may be extended to n=0,,k1n = 0, \dots, k-1 without changing its value; interchanging the two finite sums gives (ug)(k)=n=0k1i=1ku(i)(un)(ki)(ug)(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 nn, i=1ku(i)(un)(ki)=i+j=ku(i)(un)(j)=(uun)(k)=(uσ(n))(k)\sum_{i=1}^{k} u(i)(u^{n})(k-i) = \sum_{i+j=k} u(i)(u^{n})(j) = (u\,u^{n})(k) = (u^{\sigma(n)})(k), because a term of the full convolution can be nonzero only for i1i \ge 1 and j0j \ge 0; hence (ug)(k)=n=0k1(uσ(n))(k)=n=1k(un)(k)(ug)(k) = \sum_{n=0}^{k-1} (u^{\sigma(n)})(k) = \sum_{n=1}^{k} (u^{n})(k) for every k1k \ge 1.

step 1.2step 2.2step 5.1L2
7.1

For k1k \ge 1, ((1Ku)g)(k)=g(k)(ug)(k)=n=0k(un)(k)n=1k(un)(k)=(u0)(k)=1K(k)\bigl((1_K - u)g\bigr)(k) = g(k) - (ug)(k) = \sum_{n=0}^{k}(u^{n})(k) - \sum_{n=1}^{k}(u^{n})(k) = (u^{0})(k) = 1_K(k); for k=0k = 0, g(0)=(u0)(0)=1g(0) = (u^{0})(0) = 1 and (ug)(0)=0(ug)(0) = 0, so the value is 1=1K(0)1 = 1_K(0); and for k<0k < 0 both g(k)g(k) and (ug)(k)(ug)(k) are 00, as is 1K(k)1_K(k). Hence (1Ku)g=1K(1_K - u)g = 1_K.

step 3.1step 4.2step 6.1L1L2
8.1

Using [step 2.1], [L2] and cc1=1cc^{-1} = 1, one computes f(ι(c1)tpg)=ι(c)ι(c1)tpt(p)(1Ku)g=1K1K1K=1Kf \cdot \bigl(\iota(c^{-1})\,t^{p}\,g\bigr) = \iota(c)\iota(c^{-1})\, t^{-p}t^{-(-p)}\,(1_K - u)g = 1_K \cdot 1_K \cdot 1_K = 1_K, so ι(c1)tpgK\iota(c^{-1}) t^{p} g \in K is a multiplicative inverse of ff.

step 2.1step 7.1L2L4
9.1

KK is a commutative ring with 1K0K1_K \ne 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 KK 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 (un)(k)(u^{n})(k) be spoken of at all; and it is what has to be re-established for the constructed inverse, which is why gg was defined to vanish at every negative index rather than found to. The verification that this definition is consistent with (1Ku)g=1K(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)tp(1Kw)f = \iota(c')t^{-p'}(1_K - w) with c0c' \ne 0 and ww vanishing at every index 0\le 0. Evaluating as in [step 2.1] gives f(k)=c(1Kw)(kp)f(k) = c'(1_K - w)(k - p'), which is 00 for k<pk < p' and equals cc' at k=pk = p'; so p=v(f)p' = v(f) and c=lc(f)c' = \operatorname{lc}(f), and then w(j)=c1f(p+j)w(j) = -c'^{-1}f(p'+j) for j1j \ge 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((t1))\mathbb{R}((t^{-1})) is an ordered field, ordered by the sign of the leading coefficient

Statement

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

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

Facts & Assumptions

Given: KK with its valuation vv, leading coefficient lc\operatorname{lc}, constants ι(c)\iota(c) and the set PP above.

[L1]

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

[L2]

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

[L3]

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

[L5]

An ordered field is a field with a subset PP satisfying (O1) trichotomy, for each xx exactly one of xPx \in P, x=0x = 0, xP-x \in P, and (O2) closure of PP under addition and multiplication; the order is then a<b:    baPa < b :\iff b - a \in P (Ordered field). For n1n \ge 1, n1Fn \cdot 1_F is the nn-fold sum of 1F1_F, and 01F=00 \cdot 1_F = 0 (Archimedean ordered field).

[L6]

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

[L7]

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

[L8]

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

[L9]

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

Proof

technique · direct
1.1

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

L1L3L5L6
1.2

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

L3L6
1.3

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

L1L2
2.1

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

step 1.2L3L6L9
2.2

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

step 1.3L1
2.3

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

step 1.3L1L5L8
3.1

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

step 1.1step 2.1L4L5
4.1

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

step 1.1step 3.1L3L7
5.1

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

step 3.1step 2.2step 4.1step 2.3

Remarks

  • The order compares lowest terms, and only those. By clause 1, deciding f<gf < g means finding the least index at which ff and gg differ and comparing the two coefficients there. Every later coefficient is irrelevant, which is why ι(c)>t1\iota(c) > t^{-1} for every positive real cc, however small, and why the order is not the coefficientwise one.

  • R\mathbb{R} sits inside KK as an ordered subfield, and that is all clause 3 says. It does not say that R\mathbb{R} is cofinal in KK, and indeed it is not: the computation used for the canonical naturals in R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements applies verbatim to every constant, since v(t)=1<0=v(ι(c))v(t) = -1 < 0 = v(\iota(c)) for every c0c \ne 0, so ι(c)<t\iota(c) < t for every real cc. The identification n1K=ι(n1R)n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}}) is recorded because the Archimedean property is a statement about the canonical naturals (Archimedean ordered field), and it is the bridge between those and the constant series.

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

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

Statement

Let K=R((t1))K = \mathbb{R}((t^{-1})) be the ordered field of R((t1))\mathbb{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\mathbb{Z} when it is used as an index. Then:

  1. n1K<tn \cdot 1_K < t for every nNn \in \mathbb{N}; consequently KK is not Archimedean (Archimedean ordered field).
  2. 0K<t(k+1)<tk0_K < t^{-(k+1)} < t^{-k} for every kZk \in \mathbb{Z}.
  3. (Countable cofinality.) For every εK\varepsilon \in K with ε>0K\varepsilon > 0_K there is kNk \in \mathbb{N} with 0K<tk<ε0_K < t^{-k} < \varepsilon; indeed every integer k>v(ε)k > v(\varepsilon) works.
  4. (The monomials measure the valuation.) For hKh \in K and kZk \in \mathbb{Z}: if h(j)=0h(j) = 0 for every jkj \le k then h<tk|h| < t^{-k}; and conversely, if h<tk|h| < t^{-k} then h(j)=0h(j) = 0 for every j<kj < k.

Facts & Assumptions

Given: KK with its valuation vv, leading coefficient lc\operatorname{lc}, monomials tat^{-a} and constants ι(c)\iota(c).

[L1]

For nonzero hKh \in K, h(k)=0h(k) = 0 for k<v(h)k < v(h) and h(v(h))=lc(h)0h(v(h)) = \operatorname{lc}(h) \ne 0; tat^{-a} is 11 at index aa and 00 elsewhere, so ta0Kt^{-a} \ne 0_K with v(ta)=av(t^{-a}) = a and lc(ta)=1\operatorname{lc}(t^{-a}) = 1; and t=t(1)t = t^{-(-1)} (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient).

[L2]

KK is an ordered field in which f<gf < g holds exactly when gf0Kg - f \ne 0_K and lc(gf)>0\operatorname{lc}(g-f) > 0; for f0Kf \ne 0_K one has f0K|f| \ne 0_K, v(f)=v(f)v(|f|) = v(f) and lc(f)>0\operatorname{lc}(|f|) > 0; and n1K=ι(n1R)n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}}), which for n1n \ge 1 is nonzero with v=0v = 0 (R((t1))\mathbb{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,gKf, g \in K: f0K-f \ne 0_K with v(f)=v(f)v(-f) = v(f); and if v(f)<v(g)v(f) < v(g) then f+g0Kf + g \ne 0_K with lc(f+g)=lc(f)\operatorname{lc}(f+g) = \operatorname{lc}(f) (Valuation and leading coefficient in R((t1))\mathbb{R}((t^{-1})): v(fg)=v(f)+v(g)v(fg) = v(f) + v(g), and the behaviour of vv under sums).

[L4]

An ordered field FF is Archimedean when for every xFx \in F there is a natural nn with x<n1Fx < n \cdot 1_F; and in an ordered field exactly one of x<yx < y, x=yx = y, y<xy < x holds (Archimedean ordered field, Ordered field).

[L5]

The order on Z\mathbb{Z} is total, and every integer 0\ge 0 is the image of a unique natural number; so for every mZm \in \mathbb{Z} there is a natural kk whose image exceeds mm (The integers form a totally ordered ring, Order on the integers, The naturals embed in the integers).

Proof

technique · direct
1.1

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

L1L2L3
1.2

Let nNn \in \mathbb{N}. If n=0n = 0 then tn1K=tt - n \cdot 1_K = t, which is nonzero with lc(t)=1>0\operatorname{lc}(t) = 1 > 0. If n1n \ge 1 then n1Kn \cdot 1_K is nonzero with v(n1K)=0v(n \cdot 1_K) = 0, so (n1K)-(n\cdot 1_K) is nonzero with valuation 00 by [L3], while v(t)=1<0v(t) = -1 < 0; hence tn1Kt - n\cdot 1_K is nonzero with leading coefficient lc(t)=1>0\operatorname{lc}(t) = 1 > 0 by [L3]. In both cases n1K<tn \cdot 1_K < t by [L2].

L1L2L3
1.3

Conversely, let hKh \in K and kZk \in \mathbb{Z} with h<tk|h| < t^{-k}, and suppose h0Kh \ne 0_K with v(h)<kv(h) < k. Then v(h)=v(h)<k=v(tk)v(|h|) = v(h) < k = v(t^{-k}) and lc(h)>0\operatorname{lc}(|h|) > 0 by [L2], so htk|h| - t^{-k} is nonzero with leading coefficient lc(h)>0\operatorname{lc}(|h|) > 0 by [L3], giving tk<ht^{-k} < |h| and contradicting h<tk|h| < t^{-k} by the trichotomy of [L4]. Hence h=0Kh = 0_K or v(h)kv(h) \ge k, and in either case h(j)=0h(j) = 0 for every j<kj < k by [L1].

L1L2L3L4
2.1

Let hKh \in K and kZk \in \mathbb{Z} with h(j)=0h(j) = 0 for every jkj \le k. If h=0Kh = 0_K then h=0K<tk|h| = 0_K < t^{-k} by [step 1.1]. Otherwise h0Kh \ne 0_K with v(h)>kv(h) > k, so h0K|h| \ne 0_K with v(h)=v(h)>k=v(tk)v(|h|) = v(h) > k = v(t^{-k}) by [L1] and [L2]; then tkht^{-k} - |h| is nonzero with leading coefficient lc(tk)=1>0\operatorname{lc}(t^{-k}) = 1 > 0 by [L3], so h<tk|h| < t^{-k} by [L2].

step 1.1L1L2L3
2.2

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

step 1.1L1L2L3L5
2.3

By [step 1.2], n1K<tn \cdot 1_K < t for every natural nn; by the trichotomy of [L4] no natural nn can then satisfy t<n1Kt < n \cdot 1_K, so the defining condition of [L4] fails at x=tx = t and KK 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\mathbb{Z}, which has countable cofinality, and clause 3 is the translation of that fact into the order of KK: a countable family, the monomials tkt^{-k} with kNk \in \mathbb{N}, already gets below every positive element. This is what makes the sequential Cauchy condition in KK testable against countably many thresholds, and it is the reason a sequence indexed by N\mathbb{N} suffices to reach a limit in Every Cauchy sequence in R((t1))\mathbb{R}((t^{-1})) converges: KK 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 tt, not about the constants. The canonical naturals of KK are the constant series n1K=ι(n1R)n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}}) (clause 3 of R((t1))\mathbb{R}((t^{-1})) is an ordered field, ordered by the sign of the leading coefficient), all of valuation 00, and what bounds them above is tt, of valuation 1-1. The computation in step 1.2 uses nothing about tt 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((t1))\mathbb{R}((t^{-1})) does not have the least-upper-bound property; its canonical naturals have no supremum

Statement

K=R((t1))K = \mathbb{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  :=  {n1K  :  nN}    K,A \;:=\; \{\, n \cdot 1_K \;:\; n \in \mathbb{N} \,\} \;\subseteq\; K, which is nonempty and bounded above by tt, yet has no least upper bound in KK: every upper bound of AA admits a strictly smaller upper bound.

Facts & Assumptions

Given: KK with its valuation vv, leading coefficient lc\operatorname{lc}, monomials tat^{-a} and constants ι(c)\iota(c); the set A={n1K:nN}A = \{\, n \cdot 1_K : n \in \mathbb{N} \,\}.

[L1]

KK is an ordered field in which f<gf < g holds exactly when gf0Kg - f \ne 0_K and lc(gf)>0\operatorname{lc}(g-f) > 0; the canonical naturals are n1K=ι(n1R)n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}}); and for c0c \ne 0 the constant ι(c)\iota(c) is nonzero with v(ι(c))=0v(\iota(c)) = 0 and lc(ι(c))=c\operatorname{lc}(\iota(c)) = c (R((t1))\mathbb{R}((t^{-1})) is an ordered field, ordered by the sign of the leading coefficient).

[L2]
[L3]

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

[L4]

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

[L5]

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

[L6]

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

[L7]

R\mathbb{R} is a complete ordered field and hence Archimedean: for every real cc there is a natural nn with c<n1Rc < n \cdot 1_{\mathbb{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<yx < y, x=yx = y, y<xy < x holds (Ordered field).

Proof

technique · direct
1.1

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

L1L2L3L4
1.2

AA is nonempty, since 01K=0K0 \cdot 1_K = 0_K and 11K=1K1 \cdot 1_K = 1_K lie in it, and it is bounded above by tt, since n1K<tn \cdot 1_K < t for every natural nn by [L2].

L1L2L4
1.3

Let sKs \in K be any upper bound of AA. Since 1KA1_K \in A we have 1Ks1_K \le s, and 1K>0K1_K > 0_K because lc(1K)=1>0\operatorname{lc}(1_K) = 1 > 0; so s>0Ks > 0_K, hence s0Ks \ne 0_K and lc(s)>0\operatorname{lc}(s) > 0.

L1L4L5
2.1

v(s)<0v(s) < 0. Indeed, if v(s)>0v(s) > 0 then v(1K)=0<v(s)=v(s)v(1_K) = 0 < v(s) = v(-s) by [L6], so 1Ks1_K - s is nonzero with leading coefficient lc(1K)=1>0\operatorname{lc}(1_K) = 1 > 0, giving s<1Ks < 1_K and contradicting 1Ks1_K \le s by [L8]. And if v(s)=0v(s) = 0, write c:=lc(s)>0c := \operatorname{lc}(s) > 0 and use [L7] to fix a natural nn with c<n1Rc < n \cdot 1_{\mathbb{R}}; then ι(n1R)s\iota(n \cdot 1_{\mathbb{R}}) - s has both valuations equal to 00 and leading coefficients summing to n1Rc0n \cdot 1_{\mathbb{R}} - c \ne 0, so by [L6] it is nonzero with leading coefficient n1Rc>0n \cdot 1_{\mathbb{R}} - c > 0, giving n1K>sn \cdot 1_K > s and contradicting that ss is an upper bound of AA.

step 1.3L1L4L5L6L7L8
3.1

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

step 1.3step 2.1L1L5L6
4.1

ss' is an upper bound of AA: it satisfies s>0Ks' > 0_K by [L1], which settles n=0n = 0; and for n1n \ge 1 the element n1Kn \cdot 1_K is nonzero with valuation 00 by [L1], so v(s)=r<0=v((n1K))v(s') = r < 0 = v(-(n \cdot 1_K)) and [L6] makes sn1Ks' - n\cdot 1_K nonzero with leading coefficient c/2>0c/2 > 0, that is n1K<sn \cdot 1_K < s'.

step 3.1L1L5L6
4.2

s<ss' < s: both ss and s-s' are nonzero of valuation rr, and their leading coefficients sum to cc/2=c/20c - c/2 = c/2 \ne 0, so by [L6] the difference sss - s' is nonzero with leading coefficient c/2>0c/2 > 0.

step 3.1L1L6
5.1

Steps 4.1 and 4.2 show that every upper bound ss of AA admits an upper bound ss' with s<ss' < s, so no upper bound of AA is least and AA has no least upper bound in KK; with [step 1.2] this exhibits a nonempty subset of KK 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((t1))\mathbb{R}((t^{-1})) converges: KK 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 λ\lambda with 0<λ<10 < \lambda < 1 would serve in place of 1/21/2: the only properties used are that λc>0\lambda c > 0, so the smaller element is still positive of valuation r<0r < 0 and therefore still above every canonical natural, and that cλc0c - \lambda c \ne 0, so the descent is strict. Both hold for every such λ\lambda, which is why the set of upper bounds of AA 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, FF is an ordered field (Ordered field) with its order and its absolute value |\cdot| (Absolute value in an ordered field), and N\mathbb{N} is the set of natural numbers with its order (The natural numbers N\mathbb{N} (von Neumann), Order on the natural numbers).

A sequence in FF is a function x:NFx : \mathbb{N} \to F. We write xkx_k for x(k)x(k) and (xk)(x_k), or (xk)kN(x_k)_{k \in \mathbb{N}}, for the function itself.

Let (xk)(x_k) be a sequence in FF.

  • (xk)(x_k) is bounded when there is MFM \in F with xkM|x_k| \le M for every kNk \in \mathbb{N}.

  • (xk)(x_k) converges to LFL \in F when

    for every εF with ε>0 there is NN such that xkL<ε for all kN.\text{for every } \varepsilon \in F \text{ with } \varepsilon > 0 \text{ there is } N \in \mathbb{N} \text{ such that } |x_k - L| < \varepsilon \text{ for all } k \ge N.

    We then write xkLx_k \to L in FF. The sequence is convergent in FF when it converges to some LFL \in F, and divergent in FF otherwise.

  • (xk)(x_k) is Cauchy in FF when

    for every εF with ε>0 there is NN such that xkxl<ε for all k,lN.\text{for every } \varepsilon \in F \text{ with } \varepsilon > 0 \text{ there is } N \in \mathbb{N} \text{ such that } |x_k - x_l| < \varepsilon \text{ for all } k, l \ge N.

  • (xk)(x_k) is nondecreasing when xjxkx_j \le x_k for all jkj \le k, increasing when xj<xkx_j < x_k for all j<kj < k, nonincreasing when xjxkx_j \ge x_k for all jkj \le k, decreasing when xj>xkx_j > x_k for all j<kj < k, and monotone when it is nondecreasing or nonincreasing.

  • For a strictly increasing n:NNn : \mathbb{N} \to \mathbb{N}, the subsequence of (xk)(x_k) along nn is the composite (xnj)jN(x_{n_j})_{j \in \mathbb{N}}. An element LFL \in F is a subsequential limit of (xk)(x_k) when some subsequence of (xk)(x_k) converges to LL in FF.

Closed intervals and nesting. For a,bFa, b \in F with aba \le b, the closed interval with endpoints aa and bb is

[a,b]F  :=  {xF:axb},[a,b]_F \;:=\; \{\, x \in F : a \le x \le b \,\},

and its length is ba0b - a \ge 0. A sequence (Ik)kN(I_k)_{k \in \mathbb{N}} of closed intervals Ik=[ak,bk]FI_k = [a_k, b_k]_F is nested when Ik+1IkI_{k+1} \subseteq I_k for every kk. Its lengths tend to 00 in FF when the sequence (bkak)kN(b_k - a_k)_{k \in \mathbb{N}} converges to 00 in the sense above, that is, when for every ε>0\varepsilon > 0 in FF there is NNN \in \mathbb{N} with bkak<εb_k - a_k < \varepsilon for all kNk \ge N (the absolute value may be dropped because each length is 0\ge 0).

Remarks

  • The thresholds range over FF, and that is not a stylistic choice. In an Archimedean ordered field one may equivalently test ε\varepsilon over the canonical rationals, and that is what the R\mathbb{R}-specific Limits and Cauchy sequences of reals does; the two agree there, as the remark on rational and real ε\varepsilon in Sequences of reals: bounded, eventually, frequently, tails, subsequences records. In a general FF 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((t1))\mathbb{R}((t^{-1})) every positive rational constant exceeds t1t^{-1} (clause 4 of R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements, since a nonzero constant is nonzero at index 00), so the sequence taking the value 00 at even indices and t1t^{-1} at odd indices would satisfy the Cauchy condition read with rational thresholds only, while failing it at ε=t2\varepsilon = t^{-2}, where consecutive terms differ by t1>t2t^{-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 εF\varepsilon \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\mathbb{R}-notions with R\mathbb{R} replaced by FF, 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][a,b] of Intervals of R\mathbb{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\mathbb{R}-item for a general FF is a citation error. A result proved about sequences of reals is a statement about R\mathbb{R}. Many such proofs use only the ordered-field axioms and go through for any FF 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 xkLx_k \to L and xkLx_k \to L' in FF with LLL \ne L', put ε:=LL/2\varepsilon := |L - L'|/2, which is positive because LL>0|L-L'| > 0 (Basic properties of the absolute value) and 2=1+1>02 = 1 + 1 > 0. Choose NN beyond which both xkL<ε|x_k - L| < \varepsilon and xkL<ε|x_k - L'| < \varepsilon hold, and take any kNk \ge N: the triangle inequality (The triangle inequality, proved for an arbitrary ordered field) gives LLLxk+xkL<2ε=LL|L - L'| \le |L - x_k| + |x_k - L'| < 2\varepsilon = |L - L'|, which is impossible. So the limit, when it exists, is unique, and the notation limkxk\lim_k x_k is unambiguous. No completeness and no Archimedean hypothesis is used.

  • Indexing starts at 00, as everywhere in this library, because 0N0 \in \mathbb{N} (The natural numbers N\mathbb{N} (von Neumann)). A nested sequence of intervals therefore begins with I0I_0, and a statement about "the first NN terms" means the indices 0,,N10, \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((t1))\mathbb{R}((t^{-1})) converges: KK is sequentially Cauchy complete

Statement

Every sequence (f(n))nN(f^{(n)})_{n \in \mathbb{N}} in K=R((t1))K = \mathbb{R}((t^{-1})) that is Cauchy in KK (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field) converges in KK. That is, the ordered field KK of R((t1))\mathbb{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 jZj \in \mathbb{Z} the real numbers f(n)(j)f^{(n)}(j) are eventually constant in nn, and L(j)L(j) is that eventual value.

Scratch work

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

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

Second, a sequence indexed by N\mathbb{N} is long enough to reach the limit. For each of the countably many thresholds tkt^{-k} there is an index NkN_k past which the sequence is that close, and sup\sup-free bookkeeping over N\mathbb{N} assembles the NkN_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 LL must have support bounded below, so that it is an element of KK at all. That does not follow from the eventual constancy at each index separately; it comes from the single threshold k=0k = 0, which already pins down every negative index at once.

Facts & Assumptions

Given: A sequence (f(n))nN(f^{(n)})_{n \in \mathbb{N}} in KK that is Cauchy in KK.

[L1]

KK consists of the functions ZR\mathbb{Z} \to \mathbb{R} whose support is bounded below; tat^{-a} is 11 at index aa and 00 elsewhere (The formal Laurent series R((t1))\mathbb{R}((t^{-1})): support bounded below, valuation, leading coefficient).

[L3]

In KK: 0K<t(k+1)<tk0_K < t^{-(k+1)} < t^{-k} for every kZk \in \mathbb{Z}; for every ε>0\varepsilon > 0 in KK there is kNk \in \mathbb{N} with tk<εt^{-k} < \varepsilon; if h(j)=0h(j) = 0 for every jkj \le k then h<tk|h| < t^{-k}; and if h<tk|h| < t^{-k} then h(j)=0h(j) = 0 for every j<kj < k (R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements).

[L4]

(xn)(x_n) is Cauchy in KK when for every ε>0\varepsilon > 0 in KK there is NNN \in \mathbb{N} with xnxm<ε|x_n - x_m| < \varepsilon for all n,mNn, m \ge N; and (xn)(x_n) converges to LL in KK when for every ε>0\varepsilon > 0 in KK there is NN with xnL<ε|x_n - L| < \varepsilon for all nNn \ge N (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L5]

Every nonempty subset of N\mathbb{N} has a least element (The well-ordering principle).

[L6]

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

Proof

technique · constructive
1.1

For kNk \in \mathbb{N} put Mk:={NN:f(n)f(m)<t(k+1) for all n,mN}M_k := \{\, N \in \mathbb{N} : |f^{(n)} - f^{(m)}| < t^{-(k+1)} \text{ for all } n, m \ge N \,\}. Since t(k+1)>0Kt^{-(k+1)} > 0_K by [L3] and the sequence is Cauchy, MkM_k \ne \varnothing by [L4]; let Nk:=minMkN_k := \min M_k, which exists by [L5].

givenL3L4L5construct
2.1

For every kNk \in \mathbb{N}, all n,mNkn, m \ge N_k and every jkj \le k one has f(n)(j)=f(m)(j)f^{(n)}(j) = f^{(m)}(j): by [step 1.1] f(n)f(m)<t(k+1)|f^{(n)} - f^{(m)}| < t^{-(k+1)}, so [L3] gives (f(n)f(m))(j)=0(f^{(n)} - f^{(m)})(j) = 0 for every j<k+1j < k+1, that is for every jkj \le k, and (f(n)f(m))(j)=f(n)(j)f(m)(j)(f^{(n)} - f^{(m)})(j) = f^{(n)}(j) - f^{(m)}(j) by [L2].

step 1.1L2L3L6
2.2

NaNbN_a \le N_b whenever aba \le b in N\mathbb{N}: for consecutive indices, t(k+2)<t(k+1)t^{-(k+2)} < t^{-(k+1)} by [L3], so any NN witnessing membership in Mk+1M_{k+1} also witnesses membership in MkM_k by transitivity of the order [L2]; hence Mk+1MkM_{k+1} \subseteq M_k and Nk=minMkminMk+1=Nk+1N_k = \min M_k \le \min M_{k+1} = N_{k+1}. The general case follows by induction on bb [L6].

step 1.1L2L3L6
2.3

Define κ:ZN\kappa : \mathbb{Z} \to \mathbb{N} by κ(j):=j\kappa(j) := j for j0j \ge 0 and κ(j):=0\kappa(j) := 0 for j<0j < 0, so that jκ(j)j \le \kappa(j) for every jZj \in \mathbb{Z}; then define L:ZRL : \mathbb{Z} \to \mathbb{R} by L(j):=f(Nκ(j))(j)L(j) := f^{(N_{\kappa(j)})}(j).

step 1.1L6construct
3.1

For every jZj \in \mathbb{Z} and every nNκ(j)n \ge N_{\kappa(j)} one has f(n)(j)=L(j)f^{(n)}(j) = L(j): apply [step 2.1] with k=κ(j)k = \kappa(j), which is legitimate since jκ(j)j \le \kappa(j), to the two indices nn and Nκ(j)N_{\kappa(j)}, both of which are Nκ(j)\ge N_{\kappa(j)}.

step 2.1step 2.3L6
3.2

LKL \in K. The series f(N0)f^{(N_0)} lies in KK, so by [L1] there is m0Zm_0 \in \mathbb{Z} with f(N0)(j)=0f^{(N_0)}(j) = 0 for every j<m0j < m_0. If j<m0j < m_0 and j<0j < 0 then κ(j)=0\kappa(j) = 0, so L(j)=f(N0)(j)=0L(j) = f^{(N_0)}(j) = 0; hence L(j)=0L(j) = 0 for every jj below both m0m_0 and 00, the support of LL is bounded below, and LKL \in K.

step 2.3L1
4.1

For every kNk \in \mathbb{N}, every nNkn \ge N_k and every jkj \le k one has f(n)(j)=L(j)f^{(n)}(j) = L(j): if j0j \ge 0 then κ(j)=jk\kappa(j) = j \le k, and if j<0j < 0 then κ(j)=0k\kappa(j) = 0 \le k, so in both cases Nκ(j)NknN_{\kappa(j)} \le N_k \le n by [step 2.2] and [step 3.1] applies.

step 2.2step 3.1L6
5.1

(f(n))(f^{(n)}) converges to LL in KK. Let ε>0\varepsilon > 0 in KK. By [L3] — this is the countable-cofinality step, and it is the only place where anything special about KK is used — there is kNk \in \mathbb{N} with tk<εt^{-k} < \varepsilon. Put N:=NkN := N_k. For every nNn \ge N, [step 4.1] and [L2] give (f(n)L)(j)=f(n)(j)L(j)=0(f^{(n)} - L)(j) = f^{(n)}(j) - L(j) = 0 for every jkj \le k, so f(n)L<tk|f^{(n)} - L| < t^{-k} by [L3] and therefore f(n)L<ε|f^{(n)} - L| < \varepsilon by transitivity [L2]. As ε\varepsilon was arbitrary, this is convergence in the sense of [L4].

step 3.2step 4.1L2L3L4
6.1

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

step 3.2step 5.1discharge-construct

Remarks

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

R((t1))\mathbb{R}((t^{-1})) has the nested interval property for lengths tending to 00

Statement

Let K=R((t1))K = \mathbb{R}((t^{-1})) and let (In)nN(I_n)_{n \in \mathbb{N}} with In=[an,bn]KI_n = [a_n, b_n]_K be a nested sequence of closed intervals in KK whose lengths tend to 00 in KK, that is, for every ε>0\varepsilon > 0 in KK there is NN with bnan<εb_n - a_n < \varepsilon for all nNn \ge N (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field). Then

nNIn\bigcap_{n \in \mathbb{N}} I_n

contains exactly one element of KK.

The hypothesis that the lengths tend to 00 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 KK. The remarks below record what happens without the hypothesis.

Facts & Assumptions

Given: A nested sequence (In)nN(I_n)_{n \in \mathbb{N}} of closed intervals In=[an,bn]KI_n = [a_n,b_n]_K in KK, so anbna_n \le b_n and In+1InI_{n+1} \subseteq I_n for every nn, whose lengths tend to 00 in KK.

[L1]

[a,b]K={xK:axb}[a,b]_K = \{x \in K : a \le x \le b\} for aba \le b; a sequence (xn)(x_n) in KK is Cauchy in KK when for every ε>0\varepsilon > 0 in KK there is NN with xnxm<ε|x_n - x_m| < \varepsilon for all n,mNn,m \ge N, and converges to LL when for every ε>0\varepsilon > 0 in KK there is NN with xnL<ε|x_n - L| < \varepsilon for all nNn \ge N; the lengths bnanb_n - a_n tend to 00 when for every ε>0\varepsilon > 0 in KK they are eventually <ε< \varepsilon (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L3]

KK is an ordered field (R((t1))\mathbb{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<yx < y means 0<yx0 < y - x. Compatibility with addition is used below in its NONSTRICT form, xyx+zy+zx \le y \Rightarrow x + z \le y + z, whereas Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those (x<yx+z<y+zx < y \Rightarrow x + z < y + z, and x<yx < y with z<wz < w giving x+z<y+wx + z < y + w); the nonstrict form is the first strict form together with the case x=yx = y, where the two sides are equal, the order being total (Ordered field).

[L4]

z0|z| \ge 0, z=0|z| = 0 only for z=0z = 0, and z|z| equals zz or z-z; so z=z|z| = z when z0z \ge 0 (Basic properties of the absolute value, Absolute value in an ordered field).

Proof

technique · direct
1.1

For each nn, the endpoints an+1a_{n+1} and bn+1b_{n+1} belong to In+1I_{n+1} because an+1bn+1a_{n+1} \le b_{n+1}, and In+1InI_{n+1} \subseteq I_n, so both belong to InI_n; by [L1] this says anan+1a_n \le a_{n+1} and bn+1bnb_{n+1} \le b_n. Hence anan+1bn+1bna_n \le a_{n+1} \le b_{n+1} \le b_n.

givenL1L3
1.2

The intersection contains at most one element. Suppose x,ynInx, y \in \bigcap_n I_n with xyx \ne y, so xy>0|x - y| > 0 by [L4]. For each nn both xx and yy lie in [an,bn]K[a_n,b_n]_K, so xybnanx - y \le b_n - a_n and yxbnany - x \le b_n - a_n by [L1] and [L3], and since xy|x-y| is one of xyx-y, yxy-x by [L4] we get xybnan|x - y| \le b_n - a_n for every nn. Applying the shrinking hypothesis with ε:=xy\varepsilon := |x-y| produces some nn with bnan<xyb_n - a_n < |x-y|, a contradiction.

givenL1L3L4
2.1

Whenever nmn \le m one has anambmbna_n \le a_m \le b_m \le b_n: this is [step 1.1] for m=n+1m = n+1, it is trivial for m=nm = n, and the general case follows by induction on mm using transitivity of the order.

step 1.1L3L5
3.1

(an)nN(a_n)_{n \in \mathbb{N}} is Cauchy in KK. Let ε>0\varepsilon > 0 in KK and take NN with bnan<εb_n - a_n < \varepsilon for all nNn \ge N. Let n,mNn, m \ge N; by [L5] we may assume nmn \le m, the other case being the same with the roles exchanged. By [step 2.1], anambmbna_n \le a_m \le b_m \le b_n, so 0amanbnan<ε0 \le a_m - a_n \le b_n - a_n < \varepsilon, and aman=aman<ε|a_m - a_n| = a_m - a_n < \varepsilon by [L4].

step 2.1givenL1L3L4L5
4.1

By [L2] there is LKL \in K with anLa_n \to L in KK.

step 3.1L2
5.1

anLa_n \le L for every nn. Otherwise L<anL < a_n for some nn; put ε:=anL>0\varepsilon := a_n - L > 0 and use [step 4.1] to fix NN with amL<ε|a_m - L| < \varepsilon for all mNm \ge N. Pick mm with mNm \ge N and mnm \ge n ([L5]). By [step 2.1], anama_n \le a_m, so amLanL=ε>0a_m - L \ge a_n - L = \varepsilon > 0 and hence amL=amLε|a_m - L| = a_m - L \ge \varepsilon by [L4], contradicting amL<ε|a_m - L| < \varepsilon.

step 2.1step 4.1L1L3L4L5
5.2

LbnL \le b_n for every nn. Otherwise bn<Lb_n < L for some nn; put ε:=Lbn>0\varepsilon := L - b_n > 0 and fix NN with amL<ε|a_m - L| < \varepsilon for all mNm \ge N. Pick mm with mNm \ge N and mnm \ge n. By [step 2.1], ambmbna_m \le b_m \le b_n, so LamLbn=ε>0L - a_m \ge L - b_n = \varepsilon > 0 and hence amL=Lamε|a_m - L| = L - a_m \ge \varepsilon by [L4], again a contradiction.

step 2.1step 4.1L1L3L4L5
6.1

By [step 5.1] and [step 5.2], anLbna_n \le L \le b_n for every nn, so LnInL \in \bigcap_n I_n by [L1] and the intersection is nonempty; by [step 1.2] it has no second element. Hence nIn={L}\bigcap_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 KK, and The unrestricted nested interval property fails in R((t1))\mathbb{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/n2/n" does not mean shrinking. The condition is that the lengths tend to 00 in the order of KK, tested against every positive εK\varepsilon \in K, not merely against positive real constants. A nested sequence whose nn-th length is the constant series ι(2/(n+1))\iota(2/(n+1)) does not satisfy it: since ι(c)\iota(c) takes the nonzero value cc at index 00, clause 4 of R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements forbids ι(c)<t1|\iota(c)| < t^{-1}, so no such length ever gets below ε=t1\varepsilon = t^{-1}. Real-indexed shrinking is strictly weaker than shrinking in KK, 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((t1))\mathbb{R}((t^{-1})) converges: KK 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((t1))\mathbb{R}((t^{-1}))

Statement refuted

Refuted claim: the unrestricted nested interval property holds in K=R((t1))K = \mathbb{R}((t^{-1})), that is, every nested sequence I0I1I_0 \supseteq I_1 \supseteq \cdots of closed intervals In=[an,bn]KI_n = [a_n,b_n]_K of KK (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field) has nIn\bigcap_n I_n \ne \varnothing.

The witness is

an:=ι(n)t1,bn:=ι ⁣(1n+1)(nN),a_n := \iota(n)\, t^{-1}, \qquad b_n := \iota\!\left(\tfrac{1}{n+1}\right) \qquad (n \in \mathbb{N}),

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

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

Facts & Assumptions

Given: K=R((t1))K = \mathbb{R}((t^{-1})) with its valuation vv, leading coefficient lc\operatorname{lc}, monomials tat^{-a} and constants ι(c)\iota(c); and the elements an=ι(n)t1a_n = \iota(n)t^{-1}, bn=ι(1/(n+1))b_n = \iota(1/(n+1)) for nNn \in \mathbb{N}.

[L1]

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

[L2]

KK is an ordered field in which f<gf < g holds exactly when gf0Kg - f \ne 0_K and lc(gf)>0\operatorname{lc}(g-f) > 0; exactly one of f<gf < g, f=gf = g, g<fg < f holds; ι\iota is a ring homomorphism, so ι(c)+ι(d)=ι(c+d)\iota(c) + \iota(d) = \iota(c+d) and ι(c)ι(d)=ι(cd)\iota(c)\iota(d) = \iota(cd) (R((t1))\mathbb{R}((t^{-1})) is an ordered field, ordered by the sign of the leading coefficient, Ordered field).

[L3]

For nonzero f,gKf,g \in K: fg0Kfg \ne 0_K with v(fg)=v(f)+v(g)v(fg) = v(f)+v(g) and lc(fg)=lc(f)lc(g)\operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g); f0K-f \ne 0_K with v(f)=v(f)v(-f) = v(f) and lc(f)=lc(f)\operatorname{lc}(-f) = -\operatorname{lc}(f); if v(f)<v(g)v(f) < v(g) then f+g0Kf+g \ne 0_K with lc(f+g)=lc(f)\operatorname{lc}(f+g) = \operatorname{lc}(f); and if v(f)=v(g)v(f) = v(g) with lc(f)+lc(g)0\operatorname{lc}(f)+\operatorname{lc}(g) \ne 0 then f+g0Kf+g \ne 0_K with v(f+g)=v(f)v(f+g) = v(f) and lc(f+g)=lc(f)+lc(g)\operatorname{lc}(f+g) = \operatorname{lc}(f)+\operatorname{lc}(g) (Valuation and leading coefficient in R((t1))\mathbb{R}((t^{-1})): v(fg)=v(f)+v(g)v(fg) = v(f) + v(g), and the behaviour of vv under sums, R((t1))\mathbb{R}((t^{-1})) is a commutative ring: the product is a finite sum and both operations preserve support bounded below).

[L4]

0K<t(k+1)<tk0_K < t^{-(k+1)} < t^{-k} for every kZk \in \mathbb{Z}; and if h<tk|h| < t^{-k} then h(j)=0h(j) = 0 for every j<kj < k (R((t1))\mathbb{R}((t^{-1})) is non-Archimedean, and the monomials tkt^{-k} are cofinal below its positive elements).

[L5]

[a,b]K={xK:axb}[a,b]_K = \{x \in K : a \le x \le b\} for aba \le b; a sequence of closed intervals is nested when In+1InI_{n+1} \subseteq I_n for every nn; and its lengths tend to 00 in KK when for every ε>0\varepsilon > 0 in KK they are eventually <ε< \varepsilon (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L6]

R\mathbb{R} is a complete ordered field, hence Archimedean: for every real cc there is a natural nn with c<n1Rc < n \cdot 1_{\mathbb{R}}, and for every real c>0c > 0 there is a natural n1n \ge 1 with 1/n<c1/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\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon).

Counterexample

technique · direct
1.1

For n1n \ge 1 the element an=ι(n)t1a_n = \iota(n)t^{-1} is nonzero with v(an)=0+1=1v(a_n) = 0 + 1 = 1 and lc(an)=n1=n>0\operatorname{lc}(a_n) = n \cdot 1 = n > 0, while a0=ι(0)t1=0Ka_0 = \iota(0)t^{-1} = 0_K; and for every nn the element bn=ι(1/(n+1))b_n = \iota(1/(n+1)) is nonzero with v(bn)=0v(b_n) = 0 and lc(bn)=1/(n+1)>0\operatorname{lc}(b_n) = 1/(n+1) > 0. Also a1=ι(1)t1=t1a_1 = \iota(1)t^{-1} = t^{-1}.

givenL1L2L3
2.1

anbna_n \le b_n for every nn: for n=0n = 0 this is 0K<ι(1)=1K0_K < \iota(1) = 1_K, which holds since lc(1K)=1>0\operatorname{lc}(1_K) = 1 > 0; and for n1n \ge 1 we have v(bn)=0<1=v(an)v(b_n) = 0 < 1 = v(-a_n) by [step 1.1] and [L3], so bnanb_n - a_n is nonzero with leading coefficient 1/(n+1)>01/(n+1) > 0, that is an<bna_n < b_n. So each [an,bn]K[a_n,b_n]_K is a closed interval.

step 1.1L1L2L3L5
2.2

The sequence is nested: an+1an=(ι(n+1)ι(n))t1=ι(1)t1=t1>0Ka_{n+1} - a_n = \bigl(\iota(n+1) - \iota(n)\bigr)t^{-1} = \iota(1)t^{-1} = t^{-1} > 0_K by [L2] and [L4], so an<an+1a_n < a_{n+1}; and bnbn+1=ι(1n+11n+2)=ι(1(n+1)(n+2))b_n - b_{n+1} = \iota\bigl(\tfrac{1}{n+1} - \tfrac{1}{n+2}\bigr) = \iota\bigl(\tfrac{1}{(n+1)(n+2)}\bigr), which is nonzero with positive leading coefficient, so bn+1<bnb_{n+1} < b_n. Hence anan+1a_n \le a_{n+1} and bn+1bnb_{n+1} \le b_n, and every xx with an+1xbn+1a_{n+1} \le x \le b_{n+1} satisfies anxbna_n \le x \le b_n, that is In+1InI_{n+1} \subseteq I_n.

step 1.1L1L2L3L4L5
3.1

Suppose xnInx \in \bigcap_{n} I_n. Then a1xa_1 \le x, and a1=t1>0Ka_1 = t^{-1} > 0_K by [step 1.1] and [L4], so x>0Kx > 0_K; hence x0Kx \ne 0_K and lc(x)>0\operatorname{lc}(x) > 0 by [L2]. Write q:=v(x)q := v(x) and c:=lc(x)>0c := \operatorname{lc}(x) > 0.

step 1.1step 2.1L1L2L4L5
4.1

q1q \ge 1. If q<0q < 0 then v(x)<0=v(b0)v(x) < 0 = v(-b_0) by [step 1.1] and [L3], so xb0x - b_0 is nonzero with leading coefficient c>0c > 0 and x>b0x > b_0, contradicting xb0x \le b_0. If q=0q = 0, use [L6] to fix a natural n1n \ge 1 with 1/n<c1/n < c and set n:=n1n' := n - 1, so that 1/(n+1)<c1/(n'+1) < c; then xx and bn-b_{n'} both have valuation 00 with leading coefficients summing to c1/(n+1)0c - 1/(n'+1) \ne 0, so by [L3] xbnx - b_{n'} is nonzero with leading coefficient c1/(n+1)>0c - 1/(n'+1) > 0, giving x>bnx > b_{n'} and contradicting xbnx \le b_{n'}. By trichotomy on Z\mathbb{Z} the remaining case is q1q \ge 1.

step 3.1L1L2L3L5L6
4.2

q<1q < 1. If q>1q > 1 then v(a1)=1<qv(-a_1) = 1 < q by [step 1.1] and [L3], so xa1x - a_1 is nonzero with leading coefficient lc(a1)=1<0\operatorname{lc}(-a_1) = -1 < 0, giving x<a1x < a_1 and contradicting a1xa_1 \le x. If q=1q = 1, use [L6] to fix a natural nn with c<n1Rc < n \cdot 1_{\mathbb{R}}, so n1n \ge 1; then xx and an-a_n both have valuation 11 with leading coefficients summing to cn0c - n \ne 0, so by [L3] xanx - a_n is nonzero with leading coefficient cn<0c - n < 0, giving x<anx < a_n and contradicting anxa_n \le x. Hence q1q \ne 1 and q1q \not> 1.

step 3.1L1L2L3L5L6
5.1

Steps 4.1 and 4.2 are incompatible, so no xx lies in every InI_n: the nested sequence (In)(I_n) of [step 2.1] and [step 2.2] has nIn=\bigcap_n I_n = \varnothing, which refutes the unrestricted nested interval property for KK.

step 2.1step 2.2step 4.1step 4.2L5
6.1

Consistency with R((t1))\mathbb{R}((t^{-1})) has the nested interval property for lengths tending to 00: the lengths here do not tend to 00 in KK. Indeed (bnan)(0)=1/(n+1)0(b_n - a_n)(0) = 1/(n+1) \ne 0 by [step 1.1], so by [L4] the inequality bnan<t1|b_n - a_n| < t^{-1} fails for every nn; taking ε=t1\varepsilon = 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 KK. Each of the two requirements is satisfiable on its own — ι(1)\iota(1) lies above every ι(n)t1\iota(n)t^{-1}, and 0K0_K lies below every ι(1/(n+1))\iota(1/(n+1)) — yet steps 4.1 and 4.2 show that nothing in KK satisfies both at once. Both sides of the gap are approached along countable sequences, which is why intervals indexed by N\mathbb{N} can straddle it, and the lengths cannot shrink across it: they stay of valuation 00 while the left endpoints stay of valuation 11.

  • Why this does not contradict Cauchy completeness. (an)(a_n) is not Cauchy in KK: consecutive terms differ by exactly t1t^{-1}, so the Cauchy condition fails at ε=t1\varepsilon = t^{-1}. Cauchy completeness (Every Cauchy sequence in R((t1))\mathbb{R}((t^{-1})) converges: KK is sequentially Cauchy complete) constrains sequences whose terms crowd together in the order of KK, and neither endpoint sequence here does.

  • Consequence for the equivalence of completeness properties. Since KK is Cauchy complete but has neither the least-upper-bound property (R((t1))\mathbb{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 KK does satisfy is the shrinking one, and that is the form for which KK is a counterexample to the implication.

Sources