LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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.

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

Statement

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

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

Facts & Assumptions

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

[L1]

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

[L2]

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

[L3]

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

[L4]

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

[L5]

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

Proof

technique · direct

1.1

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

L1L2L3

1.2

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

L1L2L3

1.3

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

L1L2L3L4

2.1

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

step 1.1L1L2L3

2.2

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

step 1.1L1L2L3L5

2.3

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

step 1.2L4

3.1

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

step 1.1step 2.1step 1.3step 2.2step 2.3∎

Remarks

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

Depends on

Used by

Dependency tree · two levels

30 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

Archimedean property (Wikipedia) (standard reference, not scraped)
Ordered field (Wikipedia) (standard reference, not scraped)
H. G. Dales, Norming infinitesimals of large fields (standard reference, not scraped)

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