How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The Formal Laurent Series Field : Cauchy Complete, Non-Archimedean, Not Complete
1 · Prerequisites
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Foundations of the Real Numbers for Analysis
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Relations, Functions, and Quotients
- Sequences and Limits
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
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 , the formal Laurent series in over , and what is proved here is that 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 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 , 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 and does not need to. 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 is an arbitrary series in descending powers of rather than a ratio of polynomials. This page does not construct an embedding of into and never uses one; the relationship is recorded honestly in the remarks of The formal Laurent series : support bounded below, valuation, leading coefficient and is not relied on anywhere.
The construction, and the one hard algebraic step. The formal Laurent series : support bounded below, valuation, leading coefficient defines an element of as a function whose support is bounded below, written , with the valuation its lowest nonzero index and the coefficient there. 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 : , and the behaviour of under sums then records the two facts that every later argument runs on, and the behaviour of under sums, from which is at once an integral domain.
The genuinely non-trivial algebra is 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 has no notion of an infinite sum. What replaces it is the observation that vanishes at every index below when does below , 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 . is an ordered field, ordered by the sign of the leading coefficient orders by the sign of the leading coefficient: exactly when the lowest-index nonzero coefficient of 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 . is non-Archimedean, and the monomials are cofinal below its positive elements draws the consequences: exceeds every canonical natural, so is not Archimedean; the monomials decrease; and, the clause that matters most, every positive element of exceeds some with . The value group is , whose cofinality is countable, and that clause is what countable cofinality means down in the order.
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, is not, so is not complete. The concrete route names the set that fails, the canonical naturals , which are bounded above by 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 is Cauchy complete is entitled to see precisely which set has no supremum.
Sequences in a field that is not . 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 , 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 , 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 . And a theorem proved about sequences of reals is a theorem about ; it may not be cited for a general merely because its proof looks like it would transfer.
Cauchy completeness, and why the argument is not a formality. Every Cauchy sequence in converges: is sequentially Cauchy complete is the main theorem. Its hinge is the countable-cofinality clause of is non-Archimedean, and the monomials are cofinal below its positive elements: the continuum of thresholds in the Cauchy condition collapses to the countable family , so testing against those suffices, and a sequence indexed by is long enough to meet all of them. Applying the condition at says that the coefficients at all indices 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 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. has the nested interval property for lengths tending to deduces from Cauchy completeness that a nested sequence of closed intervals whose lengths tend to in the order of meets in exactly one point. The restriction is not a weakness of the proof. The unrestricted property is false in , and The unrestricted nested interval property fails in exhibits nested intervals 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 , which no element of is. The shrinking hypothesis must also be read in and not in , and both items say so. The lengths in the counterexample keep a nonzero coefficient at index , so not one of them ever gets below ; and the remarks of has the nested interval property for lengths tending to make the same point with lengths that are the real constants , which tend to in the ordinary real sense and do not tend to in 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 , and every ingredient of all three is proved on this page.
3 · Logical flowchart
4 · Definitions, theorems and proofs
The formal Laurent series : support bounded below, valuation, leading coefficient
Definition
Throughout, is the field of real numbers with its order (The real numbers, The reals form a totally ordered field) and 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 write
and say that is bounded below when there is with for every . The set of formal Laurent series in over is
equipped with
where the product sum ranges over the pairs with and . That set of pairs is finite for every , and and again lie in : this is is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗, which also proves that with these operations is a commutative ring whose zero is the constant function and whose identity is the function taking the value at and elsewhere.
Distinguished elements. For let be the function taking the value at and at every other index; so , and is the function taking the value at . For let be the function taking the value at and elsewhere. The notation is defined here as a name; that it is consistent with the ring multiplication, , is proved in is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗.
Series notation. Because is bounded below, say by , one writes
a purely notational device: the object is the function , and no convergence of any kind is asserted or used.
Valuation and leading coefficient. Let with . Then is nonempty and bounded below, so it has a least element ( is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗). Define
is the valuation and the leading coefficient of . Neither is defined at , whose support is empty; every statement about or in this library carries the hypothesis explicitly.
Order. The positive cone of is
that is, a nonzero series is positive exactly when its lowest-index nonzero coefficient is a positive real. That is an ordered field (Ordered field, Field) is is an ordered field, ordered by the sign of the leading coefficient ↗, and that every nonzero element of is invertible is is a field: every nonzero formal Laurent series is invertible ↗. As in any ordered field, means .
Remarks
-
Why the support must be bounded below. It is exactly what makes the product a finite sum. If arbitrary functions were admitted, the defining sum for would range over an infinite set of pairs and would denote nothing, since carries no notion of convergence. The condition is preserved by both operations, which is the content of is a commutative ring: the product is a finite sum and both operations preserve support bounded below ↗.
-
Indices run over all of , and the edge cases are real. The zero series has empty support and no valuation. A nonzero constant series has and , so the index is an ordinary index and not a boundary. Negative indices are admitted, and they are what makes , whose support is , an element of ; 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 smaller than every positive real constant while is larger than every real constant. The consequences are drawn in is non-Archimedean, and the monomials are cofinal below its positive elements.
-
Relation to the rational functions. The ordered field of Not every ordered field is Archimedean, ordered so that exactly when for all sufficiently large real , is the standard first example of a non-Archimedean ordered field, and standard treatments identify it with a subfield of 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 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.
is a commutative ring: the product is a finite sum and both operations preserve support bounded below
Statement
Let be as in The formal Laurent series : support bounded below, valuation, leading coefficient, and let , with chosen so that for all and for all . Then:
- (Finiteness.) For every the set is finite, so is a finite sum of reals; and whenever .
- (Closure.) , and lie in , with for and for .
- (Ring.) is a commutative ring with identity, and .
- (Monomials and constants.) for every and all ; consequently for all . Moreover for all and .
- (Least element.) Every nonempty that is bounded below has a least element. In particular has a least element whenever , so the valuation and the leading coefficient of The formal Laurent series : support bounded below, valuation, leading coefficient are defined.
Facts & Assumptions
Given: , its operations, , , the monomials and the constants as in The formal Laurent series : support bounded below, valuation, leading coefficient; elements and bounds with for and for .
consists of the functions whose support is bounded below; and ; is the zero function, is at index and elsewhere, is at index and elsewhere, and is at index and elsewhere (The formal Laurent series : support bounded below, valuation, leading coefficient).
is a totally ordered commutative ring: its order is total, and implies (The integers form a totally ordered ring, Order on the integers, Arithmetic on the integers).
Every nonempty subset of has a least element (The well-ordering principle).
The map is injective from onto the set of nonnegative integers and preserves addition and order, so every integer is for a unique natural (The naturals embed in the integers).
is a field: addition and multiplication are associative and commutative, multiplication distributes over addition, , 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
Let be nonempty with for all . Every element of is a nonnegative integer, so by [L4] for a nonempty ; by [L3] has a least element , and since preserves order and preserves order, is an element of that is every element of .
Fix and let . Then and , so and ; from and we get . Hence , and is determined by .
The integers with are in order-preserving bijection with the naturals satisfying by [L4], and there are finitely many of these, none at all when ; so is a finite set by [step 1.2], it is empty whenever , and therefore is a finite sum of reals which is whenever .
for every and for every , so and have support bounded below; and for every by [step 2.1], so does too. All three therefore lie in .
, since the two sums have the same finite index set and their terms agree by commutativity of multiplication in ; so multiplication on is commutative.
For and , expanding both and by [L1] and [L5] gives the sum of over the triples with and ; that set is finite because the argument of [step 1.2] bounds , and from below and hence, as in [step 2.1], from above as well. So multiplication on is associative.
, all three sums being finite; so multiplication distributes over addition.
For , has at most one nonzero term, the one with and , so ; taking gives , which is when and otherwise, that is, .
has at most one nonzero term, the one with and , so .
has at most one nonzero term, the one with and , so and ; moreover , so .
Addition on is defined index by index, and is closed under it and under negation by [step 3.1]; so associativity, commutativity, the law and the law each hold at every index by the corresponding law in , and is an abelian group.
By [step 4.1] addition makes an abelian group, by [step 3.2], [step 3.3] and [step 3.7] multiplication is commutative and associative with identity , and by [step 3.4] it distributes over addition; hence is a commutative ring with identity.
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 , which is nonempty when and bounded below because .
Valuation and leading coefficient in : , and the behaviour of under sums
Statement
Let with its valuation and leading coefficient (The formal Laurent series : support bounded below, valuation, leading coefficient), and let with and . Then:
- (Products.) , and In particular has no zero divisors.
- (Negatives.) , and .
- (Unequal valuations.) If then , and .
- (Equal valuations, no cancellation.) If and , then , and .
- (Sums in general.) If then .
Facts & Assumptions
Given: with and ; write and .
For a nonzero one has for every and ; conversely, if for all and then , and (The formal Laurent series : support bounded below, valuation, leading coefficient).
and , a finite sum; if vanishes at every index below and at every index below , then vanishes at every index below ( is a commutative ring: the product is a finite sum and both operations preserve support bounded below, The formal Laurent series : support bounded below, valuation, leading coefficient).
is a field, so a product of two nonzero reals is nonzero, and only for (Field, The reals form a totally ordered field).
The order on is total and compatible with addition (The integers form a totally ordered ring, Order on the integers).
Proof
By [L1] vanishes at every index below and at every index below , so by [L2] for every .
If satisfies and then and by [L1], and then forces and ; hence , which is nonzero by [L3].
for every , so vanishes exactly where does; by [L1] and [L3] this gives , and .
Suppose . For both and , so ; and because , so . By [L1], with and .
Suppose and . For both terms vanish, so ; and . By [L1], , and .
For one has , hence ; so if then its valuation, being the least index at which it is nonzero, satisfies .
By [step 1.1] vanishes at every index below and by [step 1.2] it is nonzero at ; so by [L1] , and . Since and were arbitrary nonzero elements, no product of nonzero elements of is zero.
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].
is a field: every nonzero formal Laurent series is invertible
Statement
(The formal Laurent series : support bounded below, valuation, leading coefficient) is a field (Field): it is a commutative ring with , and every with has a multiplicative inverse in .
Explicitly, if and , then for the element given by for and for , and , where vanishes at every index and is given at by .
Scratch work
The identity behind the construction is the geometric series . It cannot be used as written, because has no notion of an infinite sum. What replaces it is the observation that vanishes at every index below , so at any single index only the terms can contribute; the displayed formula for is that finite truncation, and the support of the result is bounded below because every vanishes below .
Facts & Assumptions
Given: A nonzero ; write and , so that for every and .
is the set of functions whose support is bounded below; is at index and elsewhere; is at index and elsewhere; for nonzero one has for and (The formal Laurent series : support bounded below, valuation, leading coefficient).
is a commutative ring with identity ; is a finite sum; if vanishes at every index and at every index then vanishes at every index ; and hence ; and ( is a commutative ring: the product is a finite sum and both operations preserve support bounded below).
A product of two nonzero elements of is nonzero (Valuation and leading coefficient in : , and the behaviour of under sums).
is a field: every nonzero has an inverse with , and a finite sum of reals may be reordered and regrouped freely (Field, The reals form a totally ordered field).
Recursion on : for a set , an element and a function there is a unique with and (The recursion theorem, The natural numbers (von Neumann)).
Induction: a property holding at and inherited from to holds at every natural number (The principle of mathematical induction).
A field is a commutative ring with 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
Define by for and for . Then vanishes at every index , so its support is bounded below and .
By [L5] with , and there is a family in with and .
For every , by [L2]; this is when because vanishes at every negative index, it is when , and it is when . Comparing with for and , we get .
For every , vanishes at every index : at this says vanishes at every negative index, which holds by [L1]; and if vanishes at every index then, since vanishes at every index by [step 1.1], the product vanishes at every index by [L2].
Define by for and for ; each value is a finite sum of reals, and vanishes at every index , so .
Fix . In a term can be nonzero only when and , hence only for and ; so .
For one has , since vanishes at every index and at every index , so every pair with has .
In the inner sum of [step 4.1] the terms with vanish by [step 2.2], so the inner sum may be extended to without changing its value; interchanging the two finite sums gives .
For each , , because a term of the full convolution can be nonzero only for and ; hence for every .
For , ; for , and , so the value is ; and for both and are , as is . Hence .
Using [step 2.1], [L2] and , one computes , so is a multiplicative inverse of .
is a commutative ring with by [L2], its nonzero elements are closed under multiplication by [L3], and by [step 8.1] every nonzero element has an inverse; so satisfies the field axioms of [L7] and the construction is complete.
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 be spoken of at all; and it is what has to be re-established for the constructed inverse, which is why was defined to vanish at every negative index rather than found to. The verification that this definition is consistent with 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 with and vanishing at every index . Evaluating as in [step 2.1] gives , which is for and equals at ; so and , and then for . 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.
is an ordered field, ordered by the sign of the leading coefficient
Statement
Let and let (The formal Laurent series : support bounded below, valuation, leading coefficient). Then:
- is a positive cone on , so is an ordered field (Ordered field), and holds exactly when and .
- For the absolute value (Absolute value in an ordered field) satisfies , and .
- The map sending to the series with value at index is an injective ring homomorphism with exactly when ; and the canonical naturals of are for every .
Facts & Assumptions
Given: with its valuation , leading coefficient , constants and the set above.
For nonzero , for and ; is at index and elsewhere; (The formal Laurent series : support bounded below, valuation, leading coefficient).
is a commutative ring, , and ( is a commutative ring: the product is a finite sum and both operations preserve support bounded below).
For nonzero : with ; with and ; if then with and ; and if with then with (Valuation and leading coefficient in : , and the behaviour of under sums).
is a field ( is a field: every nonzero formal Laurent series is invertible, Field).
An ordered field is a field with a subset satisfying (O1) trichotomy, for each exactly one of , , , and (O2) closure of under addition and multiplication; the order is then (Ordered field). For , is the -fold sum of , and (Archimedean ordered field).
is an ordered field: exactly one of , , holds for each real , and sums and products of positive reals are positive (The reals form a totally ordered field, Ordered field).
when and when , in any ordered field and in (Absolute value in an ordered field).
Induction: a property holding at and inherited from to holds at every natural number (The principle of mathematical induction, The natural numbers (von Neumann)).
The order on is total, so for exactly one of , , holds (The integers form a totally ordered ring).
Proof
Let . If then neither nor lies in , since membership in requires being nonzero. If then and by [L3], and by trichotomy in ([L6]) exactly one of and holds. So for every exactly one of , , holds, which is (O1).
Let . By [L3] and , a product of two positive reals, hence positive by [L6]; so .
because addition is computed index by index, and because by [L2], which is at and elsewhere; also , and is injective since .
Let and compare with , which by [L9] are related in exactly one of three ways. If then by [L3] and ; if the same argument with the roles exchanged applies; and if then by [L6], in particular nonzero, so by [L3] and . In every case , which with [step 1.2] is (O2).
For the series is nonzero with and , so exactly when ; and . With [step 1.3] this makes an injective ring homomorphism carrying the positive reals onto the positive constants.
For every natural , : at both sides are by [L5] and [L1], and if the identity holds at then by [step 1.3].
By [step 1.1] and [step 2.1] the set satisfies (O1) and (O2), and is a field by [L4]; hence is an ordered field, in which means , that is, and .
Let . If then by [step 3.1], so by [L7], and since . Otherwise by [step 1.1], so and , whence , and , again positive. In both cases and .
Clause 1 is [step 3.1], clause 2 is [step 4.1], and clause 3 is [step 2.2] with [step 2.3].
Remarks
-
The order compares lowest terms, and only those. By clause 1, deciding means finding the least index at which and differ and comparing the two coefficients there. Every later coefficient is irrelevant, which is why for every positive real , however small, and why the order is not the coefficientwise one.
-
sits inside as an ordered subfield, and that is all clause 3 says. It does not say that is cofinal in , and indeed it is not: the computation used for the canonical naturals in is non-Archimedean, and the monomials are cofinal below its positive elements applies verbatim to every constant, since for every , so for every real . The identification 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.
is non-Archimedean, and the monomials are cofinal below its positive elements
Statement
Let be the ordered field of is an ordered field, ordered by the sign of the leading coefficient, and identify a natural number with its image in when it is used as an index. Then:
- for every ; consequently is not Archimedean (Archimedean ordered field).
- for every .
- (Countable cofinality.) For every with there is with ; indeed every integer works.
- (The monomials measure the valuation.) For and : if for every then ; and conversely, if then for every .
Facts & Assumptions
Given: with its valuation , leading coefficient , monomials and constants .
For nonzero , for and ; is at index and elsewhere, so with and ; and (The formal Laurent series : support bounded below, valuation, leading coefficient).
is an ordered field in which holds exactly when and ; for one has , and ; and , which for is nonzero with ( is an ordered field, ordered by the sign of the leading coefficient, Absolute value in an ordered field).
For nonzero : with ; and if then with (Valuation and leading coefficient in : , and the behaviour of under sums).
An ordered field is Archimedean when for every there is a natural with ; and in an ordered field exactly one of , , holds (Archimedean ordered field, Ordered field).
The order on is total, and every integer is the image of a unique natural number; so for every there is a natural whose image exceeds (The integers form a totally ordered ring, Order on the integers, The naturals embed in the integers).
Proof
For every the monomial is nonzero with , so by [L2]; and since by [L1] and [L3], the difference is nonzero with leading coefficient , so .
Let . If then , which is nonzero with . If then is nonzero with , so is nonzero with valuation by [L3], while ; hence is nonzero with leading coefficient by [L3]. In both cases by [L2].
Conversely, let and with , and suppose with . Then and by [L2], so is nonzero with leading coefficient by [L3], giving and contradicting by the trichotomy of [L4]. Hence or , and in either case for every by [L1].
Let and with for every . If then by [step 1.1]. Otherwise with , so with by [L1] and [L2]; then is nonzero with leading coefficient by [L3], so by [L2].
Let with , so and by [L2]; put and use [L5] to fix a natural with . Then by [L1] and [L3], so is nonzero with leading coefficient , that is ; and by [step 1.1]. The same computation applies to every integer .
By [step 1.2], for every natural ; by the trichotomy of [L4] no natural can then satisfy , so the defining condition of [L4] fails at and is not Archimedean.
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].
Remarks
-
Why clause 3 is the pivotal one. The valuation takes its values in , which has countable cofinality, and clause 3 is the translation of that fact into the order of : a countable family, the monomials with , already gets below every positive element. This is what makes the sequential Cauchy condition in testable against countably many thresholds, and it is the reason a sequence indexed by suffices to reach a limit in Every Cauchy sequence in converges: 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 , not about the constants. The canonical naturals of are the constant series (clause 3 of is an ordered field, ordered by the sign of the leading coefficient), all of valuation , and what bounds them above is , of valuation . The computation in step 1.2 uses nothing about 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.
does not have the least-upper-bound property; its canonical naturals have no supremum
Statement
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 which is nonempty and bounded above by , yet has no least upper bound in : every upper bound of admits a strictly smaller upper bound.
Facts & Assumptions
Given: with its valuation , leading coefficient , monomials and constants ; the set .
is an ordered field in which holds exactly when and ; the canonical naturals are ; and for the constant is nonzero with and ( is an ordered field, ordered by the sign of the leading coefficient).
for every , and is not Archimedean ( is non-Archimedean, and the monomials are cofinal below its positive elements, Archimedean ordered field).
Every complete ordered field is Archimedean (Every complete ordered field is Archimedean).
is a complete ordered field when every nonempty that is bounded above has a least upper bound in , a least upper bound being an upper bound every upper bound (Complete ordered field (least-upper-bound property)).
For nonzero : for and ; is nonzero with and (The formal Laurent series : support bounded below, valuation, leading coefficient).
For nonzero : with and ; with and ; if then with ; and if with then with and (Valuation and leading coefficient in : , and the behaviour of under sums).
is a complete ordered field and hence Archimedean: for every real there is a natural with (The reals form a totally ordered field, The Cauchy-sequence reals have the least-upper-bound property, Every complete ordered field is Archimedean).
In an ordered field exactly one of , , holds (Ordered field).
Proof
is an ordered field that is not Archimedean, while by [L3] every complete ordered field is Archimedean; so is not a complete ordered field, that is, does not have the least-upper-bound property of [L4].
is nonempty, since and lie in it, and it is bounded above by , since for every natural by [L2].
Let be any upper bound of . Since we have , and because ; so , hence and .
. Indeed, if then by [L6], so is nonzero with leading coefficient , giving and contradicting by [L8]. And if , write and use [L7] to fix a natural with ; then has both valuations equal to and leading coefficients summing to , so by [L6] it is nonzero with leading coefficient , giving and contradicting that is an upper bound of .
Put and , and set . By [L1], [L5] and [L6], is nonzero with and .
is an upper bound of : it satisfies by [L1], which settles ; and for the element is nonzero with valuation by [L1], so and [L6] makes nonzero with leading coefficient , that is .
: both and are nonzero of valuation , and their leading coefficients sum to , so by [L6] the difference is nonzero with leading coefficient .
Steps 4.1 and 4.2 show that every upper bound of admits an upper bound with , so no upper bound of is least and has no least upper bound in ; with [step 1.2] this exhibits a nonempty subset of that is bounded above and has no supremum, which is the concrete form of the failure already established in [step 1.1].
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 converges: 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 would serve in place of : the only properties used are that , so the smaller element is still positive of valuation and therefore still above every canonical natural, and that , so the descent is strict. Both hold for every such , which is why the set of upper bounds of has no least element rather than merely failing to contain one particular candidate.
Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field
Definition
Throughout, is an ordered field (Ordered field) with its order and its absolute value (Absolute value in an ordered field), and is the set of natural numbers with its order (The natural numbers (von Neumann), Order on the natural numbers).
A sequence in is a function . We write for and , or , for the function itself.
Let be a sequence in .
-
is bounded when there is with for every .
-
converges to when
We then write in . The sequence is convergent in when it converges to some , and divergent in otherwise.
-
is Cauchy in when
-
is nondecreasing when for all , increasing when for all , nonincreasing when for all , decreasing when for all , and monotone when it is nondecreasing or nonincreasing.
-
For a strictly increasing , the subsequence of along is the composite . An element is a subsequential limit of when some subsequence of converges to in .
Closed intervals and nesting. For with , the closed interval with endpoints and is
and its length is . A sequence of closed intervals is nested when for every . Its lengths tend to in when the sequence converges to in the sense above, that is, when for every in there is with for all (the absolute value may be dropped because each length is ).
Remarks
-
The thresholds range over , 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 -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 they do not agree, because the canonical rationals need not be cofinal below the positive elements. A concrete failure lives on this page: in every positive rational constant exceeds (clause 4 of is non-Archimedean, and the monomials are cofinal below its positive elements, since a nonzero constant is nonzero at index ), so the sequence taking the value at even indices and at odd indices would satisfy the Cauchy condition read with rational thresholds only, while failing it at , where consecutive terms differ by ; and it has no limit at all, since a convergent sequence is Cauchy by the triangle inequality. Every definition above therefore quantifies over , 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 -notions with replaced by , 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 of Intervals of : 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 -item for a general is a citation error. A result proved about sequences of reals is a statement about . Many such proofs use only the ordered-field axioms and go through for any 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 and in with , put , which is positive because (Basic properties of the absolute value) and . Choose beyond which both and hold, and take any : the triangle inequality (The triangle inequality, proved for an arbitrary ordered field) gives , which is impossible. So the limit, when it exists, is unique, and the notation is unambiguous. No completeness and no Archimedean hypothesis is used.
-
Indexing starts at , as everywhere in this library, because (The natural numbers (von Neumann)). A nested sequence of intervals therefore begins with , and a statement about "the first terms" means the indices .
Every Cauchy sequence in converges: is sequentially Cauchy complete
Statement
Every sequence in that is Cauchy in (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field) converges in . That is, the ordered field of 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 the real numbers are eventually constant in , and is that eventual value.
Scratch work
The whole theorem turns on one structural fact about , and it is worth isolating before the proof: the value group is , so it has countable cofinality. Concretely, the countably many monomials , , get below every positive element of ( is non-Archimedean, and the monomials are cofinal below its positive elements, clause 3). Two consequences drive everything.
First, the Cauchy condition, which quantifies over the uncountably many positive , is equivalent to its restriction to the countable family , and by clause 4 of the same lemma that restricted condition says exactly: for each the coefficients at all indices are eventually constant along the sequence.
Second, a sequence indexed by is long enough to reach the limit. For each of the countably many thresholds there is an index past which the sequence is that close, and -free bookkeeping over assembles the 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 must have support bounded below, so that it is an element of at all. That does not follow from the eventual constancy at each index separately; it comes from the single threshold , which already pins down every negative index at once.
Facts & Assumptions
Given: A sequence in that is Cauchy in .
consists of the functions whose support is bounded below; is at index and elsewhere (The formal Laurent series : support bounded below, valuation, leading coefficient).
is an ordered field, so its order is transitive and total ( is an ordered field, ordered by the sign of the leading coefficient, Ordered field, Absolute value in an ordered field); and for ( is a commutative ring: the product is a finite sum and both operations preserve support bounded below).
In : for every ; for every in there is with ; if for every then ; and if then for every ( is non-Archimedean, and the monomials are cofinal below its positive elements).
is Cauchy in when for every in there is with for all ; and converges to in when for every in there is with for all (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).
Every nonempty subset of has a least element (The well-ordering principle).
The order on is total ( is a linear order on , Order on the natural numbers), induction is available (The principle of mathematical induction, The natural numbers (von Neumann)), and every integer is the image of a unique natural number, so a natural number may be used as an index in (The naturals embed in the integers).
Proof
For put . Since by [L3] and the sequence is Cauchy, by [L4]; let , which exists by [L5].
For every , all and every one has : by [step 1.1] , so [L3] gives for every , that is for every , and by [L2].
whenever in : for consecutive indices, by [L3], so any witnessing membership in also witnesses membership in by transitivity of the order [L2]; hence and . The general case follows by induction on [L6].
Define by for and for , so that for every ; then define by .
For every and every one has : apply [step 2.1] with , which is legitimate since , to the two indices and , both of which are .
. The series lies in , so by [L1] there is with for every . If and then , so ; hence for every below both and , the support of is bounded below, and .
For every , every and every one has : if then , and if then , so in both cases by [step 2.2] and [step 3.1] applies.
converges to in . Let in . By [L3] — this is the countable-cofinality step, and it is the only place where anything special about is used — there is with . Put . For every , [step 4.1] and [L2] give for every , so by [L3] and therefore by transitivity [L2]. As was arbitrary, this is convergence in the sense of [L4].
The sequence was an arbitrary Cauchy sequence in , and [step 3.2] and [step 5.1] produce an element to which it converges; so every Cauchy sequence in converges in .
Remarks
-
What makes the argument work, in one sentence. The value group of is , whose cofinality is countable, so the continuum of thresholds in the Cauchy condition collapses to the countable family , ( is non-Archimedean, and the monomials are cofinal below its positive elements, clause 3), and a sequence indexed by 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 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 is eventually constant gives a function 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 freezes all indices simultaneously from the single stage onward, so agrees with the one series on the whole negative half-line and inherits its lower bound.
-
No choice is used. The stage is not chosen: it is defined as the least element of , 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 " would be an appeal to countable choice for no reason.
-
This is Cauchy completeness and nothing more. is sequentially Cauchy complete and at the same time lacks the least-upper-bound property ( 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 has the nested interval property for lengths tending to for what it does give, and The unrestricted nested interval property fails in for what it does not.
has the nested interval property for lengths tending to
Statement
Let and let with be a nested sequence of closed intervals in whose lengths tend to in , that is, for every in there is with for all (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field). Then
contains exactly one element of .
The hypothesis that the lengths tend to 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 . The remarks below record what happens without the hypothesis.
Facts & Assumptions
Given: A nested sequence of closed intervals in , so and for every , whose lengths tend to in .
for ; a sequence in is Cauchy in when for every in there is with for all , and converges to when for every in there is with for all ; the lengths tend to when for every in they are eventually (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).
Every Cauchy sequence in converges in (Every Cauchy sequence in converges: is sequentially Cauchy complete).
is an ordered field ( is an ordered field, ordered by the sign of the leading coefficient, Ordered field), so its order is total and transitive and means . Compatibility with addition is used below in its NONSTRICT form, , whereas Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those (, and with giving ); the nonstrict form is the first strict form together with the case , where the two sides are equal, the order being total (Ordered field).
, only for , and equals or ; so when (Basic properties of the absolute value, Absolute value in an ordered field).
The order on is total ( is a linear order on , Order on the natural numbers) and induction is available (The principle of mathematical induction, The natural numbers (von Neumann)).
Proof
For each , the endpoints and belong to because , and , so both belong to ; by [L1] this says and . Hence .
The intersection contains at most one element. Suppose with , so by [L4]. For each both and lie in , so and by [L1] and [L3], and since is one of , by [L4] we get for every . Applying the shrinking hypothesis with produces some with , a contradiction.
Whenever one has : this is [step 1.1] for , it is trivial for , and the general case follows by induction on using transitivity of the order.
is Cauchy in . Let in and take with for all . Let ; by [L5] we may assume , the other case being the same with the roles exchanged. By [step 2.1], , so , and by [L4].
By [L2] there is with in .
for every . Otherwise for some ; put and use [step 4.1] to fix with for all . Pick with and ([L5]). By [step 2.1], , so and hence by [L4], contradicting .
for every . Otherwise for some ; put and fix with for all . Pick with and . By [step 2.1], , so and hence by [L4], again a contradiction.
By [step 5.1] and [step 5.2], for every , so by [L1] and the intersection is nonempty; by [step 1.2] it has no second element. Hence .
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 , and The unrestricted nested interval property fails in 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 " does not mean shrinking. The condition is that the lengths tend to in the order of , tested against every positive , not merely against positive real constants. A nested sequence whose -th length is the constant series does not satisfy it: since takes the nonzero value at index , clause 4 of is non-Archimedean, and the monomials are cofinal below its positive elements forbids , so no such length ever gets below . Real-indexed shrinking is strictly weaker than shrinking in , 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 converges: is sequentially Cauchy complete and not an independent argument about series.
5 · Examples, counterexamples and false statements
The unrestricted nested interval property fails in
Statement refuted
Refuted claim: the unrestricted nested interval property holds in , that is, every nested sequence of closed intervals of (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field) has .
The witness is
where is the constant series with value at index and abbreviates (The formal Laurent series : support bounded below, valuation, leading coefficient). The intervals are nested and their intersection is empty: a common point would have to be an infinitesimal of valuation , because it lies below every positive real constant, and simultaneously not such an element, because it lies above every multiple of .
This refutes only the unrestricted form. The shrinking form, with the additional hypothesis that the lengths tend to in , is true ( has the nested interval property for lengths tending to ), and the lengths here do not tend to .
Facts & Assumptions
Given: with its valuation , leading coefficient , monomials and constants ; and the elements , for .
For nonzero : for and ; is nonzero with and ; and for is nonzero with and (The formal Laurent series : support bounded below, valuation, leading coefficient, is an ordered field, ordered by the sign of the leading coefficient).
is an ordered field in which holds exactly when and ; exactly one of , , holds; is a ring homomorphism, so and ( is an ordered field, ordered by the sign of the leading coefficient, Ordered field).
For nonzero : with and ; with and ; if then with ; and if with then with and (Valuation and leading coefficient in : , and the behaviour of under sums, is a commutative ring: the product is a finite sum and both operations preserve support bounded below).
for every ; and if then for every ( is non-Archimedean, and the monomials are cofinal below its positive elements).
for ; a sequence of closed intervals is nested when for every ; and its lengths tend to in when for every in they are eventually (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).
is a complete ordered field, hence Archimedean: for every real there is a natural with , and for every real there is a natural with (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 in a complete ordered field there is a natural with ).
Counterexample
For the element is nonzero with and , while ; and for every the element is nonzero with and . Also .
for every : for this is , which holds since ; and for we have by [step 1.1] and [L3], so is nonzero with leading coefficient , that is . So each is a closed interval.
The sequence is nested: by [L2] and [L4], so ; and , which is nonzero with positive leading coefficient, so . Hence and , and every with satisfies , that is .
Suppose . Then , and by [step 1.1] and [L4], so ; hence and by [L2]. Write and .
. If then by [step 1.1] and [L3], so is nonzero with leading coefficient and , contradicting . If , use [L6] to fix a natural with and set , so that ; then and both have valuation with leading coefficients summing to , so by [L3] is nonzero with leading coefficient , giving and contradicting . By trichotomy on the remaining case is .
. If then by [step 1.1] and [L3], so is nonzero with leading coefficient , giving and contradicting . If , use [L6] to fix a natural with , so ; then and both have valuation with leading coefficients summing to , so by [L3] is nonzero with leading coefficient , giving and contradicting . Hence and .
Steps 4.1 and 4.2 are incompatible, so no lies in every : the nested sequence of [step 2.1] and [step 2.2] has , which refutes the unrestricted nested interval property for .
Consistency with has the nested interval property for lengths tending to : the lengths here do not tend to in . Indeed by [step 1.1], so by [L4] the inequality fails for every ; taking shows the shrinking hypothesis of [L5] is not satisfied.
Remarks
-
What the counterexample really exhibits. It is a gap in . Each of the two requirements is satisfiable on its own — lies above every , and lies below every — yet steps 4.1 and 4.2 show that nothing in satisfies both at once. Both sides of the gap are approached along countable sequences, which is why intervals indexed by can straddle it, and the lengths cannot shrink across it: they stay of valuation while the left endpoints stay of valuation .
-
Why this does not contradict Cauchy completeness. is not Cauchy in : consecutive terms differ by exactly , so the Cauchy condition fails at . Cauchy completeness (Every Cauchy sequence in converges: is sequentially Cauchy complete) constrains sequences whose terms crowd together in the order of , and neither endpoint sequence here does.
-
Consequence for the equivalence of completeness properties. Since is Cauchy complete but has neither the least-upper-bound property ( 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 does satisfy is the shrinking one, and that is the form for which is a counterexample to the implication.
Sources
Standard references
Recommended treatments; not extraction sources.
- Formal power series (Wikipedia)
- Hahn series (Wikipedia)
- Ordered field (Wikipedia)
- B. Sambale, An invitation to formal power series
- H. G. Dales, Norming infinitesimals of large fields
- Valuation (algebra) (Wikipedia)
- Laurent series (Encyclopedia of Mathematics)
- Archimedean property (Wikipedia)
- Complete ordered fields are Archimedean (Rutgers Math 311 notes)
- Cauchy sequence (Wikipedia)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1
- Cauchy sequences in ordered fields (University of Tennessee notes)
- Complete field (Wikipedia)
- Nested intervals (Wikipedia)
- Cantor theorem (Encyclopedia of Mathematics)