LemmaStatement: AI-adaptedProof: AI-generatedSession-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}))$ is non-Archimedean, and the monomials $t^{-k}$ are cofinal below its positive elements

Statement

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

$n \cdot 1_K < t$ for every $n \in \mathbb{N}$ ; consequently $K$ is not Archimedean (Archimedean ordered field).
$0_K < t^{-(k+1)} < t^{-k}$ for every $k \in \mathbb{Z}$ .
(Countable cofinality.) For every $\varepsilon \in K$ with $\varepsilon > 0_K$ there is $k \in \mathbb{N}$ with $0_K < t^{-k} < \varepsilon$ ; indeed every integer $k > v(\varepsilon)$ works.
(The monomials measure the valuation.) For $h \in K$ and $k \in \mathbb{Z}$ : if $h(j) = 0$ for every $j \le 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 $\operatorname{lc}$ , monomials $t^{-a}$ and constants $\iota(c)$ .

[L1]

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

[L2]

$K$ is an ordered field in which $f < g$ holds exactly when $g - f \ne 0_K$ and $\operatorname{lc}(g-f) > 0$ ; for $f \ne 0_K$ one has $|f| \ne 0_K$ , $v(|f|) = v(f)$ and $\operatorname{lc}(|f|) > 0$ ; and $n \cdot 1_K = \iota(n \cdot 1_{\mathbb{R}})$ , which for $n \ge 1$ is nonzero with $v = 0$ ( $\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, g \in K$ : $-f \ne 0_K$ with $v(-f) = v(f)$ ; and if $v(f) < v(g)$ then $f + g \ne 0_K$ with $\operatorname{lc}(f+g) = \operatorname{lc}(f)$ (Valuation and leading coefficient in $\mathbb{R}((t^{-1}))$ : $v(fg) = 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 $\mathbb{Z}$ is total, and every integer $\ge 0$ is the image of a unique natural number; so for every $m \in \mathbb{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 \mathbb{Z}$ the monomial $t^{-k}$ is nonzero with $\operatorname{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 $\operatorname{lc}(t^{-k}) = 1 > 0$ , so $t^{-(k+1)} < t^{-k}$ .

L1L2L3

1.2

Let $n \in \mathbb{N}$ . If $n = 0$ then $t - n \cdot 1_K = t$ , which is nonzero with $\operatorname{lc}(t) = 1 > 0$ . If $n \ge 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 $\operatorname{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 \mathbb{Z}$ with $|h| < t^{-k}$ , and suppose $h \ne 0_K$ with $v(h) < k$ . Then $v(|h|) = v(h) < k = v(t^{-k})$ and $\operatorname{lc}(|h|) > 0$ by [L2], so $|h| - t^{-k}$ is nonzero with leading coefficient $\operatorname{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) \ge k$ , and in either case $h(j) = 0$ for every $j < k$ by [L1].

L1L2L3L4

2.1

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

step 1.1L1L2L3

2.2

Let $\varepsilon \in K$ with $\varepsilon > 0_K$ , so $\varepsilon \ne 0_K$ and $\operatorname{lc}(\varepsilon) > 0$ by [L2]; put $m := v(\varepsilon)$ and use [L5] to fix a natural $k$ with $k > m$ . Then $v(\varepsilon) = m < k = v(t^{-k}) = v(-t^{-k})$ by [L1] and [L3], so $\varepsilon - t^{-k}$ is nonzero with leading coefficient $\operatorname{lc}(\varepsilon) > 0$ , that is $t^{-k} < \varepsilon$ ; 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 $\mathbb{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 \mathbb{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 $\mathbb{N}$ suffices to reach a limit in Every Cauchy sequence in $\mathbb{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 = \iota(n \cdot 1_{\mathbb{R}})$ (clause 3 of $\mathbb{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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 results over 24 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

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))\mathbb{R}((t^{-1}))R((t−1)) is non-Archimedean, and the monomials t−kt^{-k}t−k are cofinal below its positive elements