CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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

Statement

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

Facts & Assumptions

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

[L1]

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

[L2]

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

[L3]

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

[L4]

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

[L5]

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

[L6]

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

[L7]

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

Proof

technique · direct

1.1

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

L1L2L3L4

1.2

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

L1L2L4

1.3

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

L1L4L5

2.1

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

step 1.3L1L4L5L6L7L8

3.1

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

step 1.3step 2.1L1L5L6

4.1

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

step 3.1L1L5L6

4.2

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

step 3.1L1L6

5.1

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

step 1.1step 1.2step 4.1step 4.2L4∎

Remarks

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

Depends on

Used by

Dependency tree · next 3 levels

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

Sources

Ordered field (Wikipedia) (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)
Complete ordered fields are Archimedean (Rutgers Math 311 notes) (standard reference, not scraped)
H. G. Dales, Norming infinitesimals of large fields (standard reference, not scraped)

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