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

How statement and proof provenance work

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

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

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

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

Statement

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

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

Scratch work

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

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

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

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

Facts & Assumptions

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

[L1]

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

[L2]

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

[L3]

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

[L4]

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

[L5]

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

[L6]

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

Proof

technique · constructive

1.1

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

givenL3L4L5construct

2.1

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

step 1.1L2L3L6

2.2

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

step 1.1L2L3L6

2.3

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

step 1.1L6construct

3.1

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

step 2.1step 2.3L6

3.2

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

step 2.3L1

4.1

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

step 2.2step 3.1L6

5.1

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

step 3.2step 4.1L2L3L4

6.1

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

step 3.2step 5.1discharge-construct∎

Remarks

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

Depends on

Used by

Dependency tree · two levels

46 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hahn series (Wikipedia) (standard reference, not scraped)
Cauchy sequence (Wikipedia) (standard reference, not scraped)
Complete field (Wikipedia) (standard reference, not scraped)
B. Sambale, An invitation to formal power series (standard reference, not scraped)
Laurent series (Encyclopedia of Mathematics) (standard reference, not scraped)
H. G. Dales, Norming infinitesimals of large fields (standard reference, not scraped)

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