LemmaStatement: 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.

Valuation and leading coefficient in $\mathbb{R}((t^{-1}))$ : $v(fg) = v(f) + v(g)$ , and the behaviour of $v$ under sums

Statement

Let $K = \mathbb{R}((t^{-1}))$ with its valuation $v$ and leading coefficient $\operatorname{lc}$ (The formal Laurent series $\mathbb{R}((t^{-1}))$ : support bounded below, valuation, leading coefficient), and let $f, g \in K$ with $f \ne 0_K$ and $g \ne 0_K$ . Then:

(Products.) $fg \ne 0_K$ , and $v(fg) = v(f) + v(g), \qquad \operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g).$ In particular $K$ has no zero divisors.
(Negatives.) $-f \ne 0_K$ , $v(-f) = v(f)$ and $\operatorname{lc}(-f) = -\operatorname{lc}(f)$ .
(Unequal valuations.) If $v(f) < v(g)$ then $f + g \ne 0_K$ , $v(f+g) = v(f)$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f)$ .
(Equal valuations, no cancellation.) If $v(f) = v(g) = q$ and $\operatorname{lc}(f) + \operatorname{lc}(g) \ne 0$ , then $f + g \ne 0_K$ , $v(f+g) = q$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f) + \operatorname{lc}(g)$ .
(Sums in general.) If $f + g \ne 0_K$ then $v(f+g) \ge \min\{v(f), v(g)\}$ .

Facts & Assumptions

Given: $f, g \in K$ with $f \ne 0_K$ and $g \ne 0_K$ ; write $p := v(f)$ and $q := v(g)$ .

[L1]

For a nonzero $h \in K$ one has $h(k) = 0$ for every $k < v(h)$ and $h(v(h)) = \operatorname{lc}(h) \ne 0$ ; conversely, if $h(k) = 0$ for all $k < r$ and $h(r) \ne 0$ then $h \ne 0_K$ , $v(h) = r$ and $\operatorname{lc}(h) = h(r)$ (The formal Laurent series $\mathbb{R}((t^{-1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$(f+g)(k) = f(k) + g(k)$ and $(fg)(k) = \sum_{i+j=k} f(i)g(j)$ , a finite sum; if $f$ vanishes at every index below $m$ and $g$ at every index below $n$ , then $fg$ vanishes at every index below $m+n$ ( $\mathbb{R}((t^{-1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below, The formal Laurent series $\mathbb{R}((t^{-1}))$ : support bounded below, valuation, leading coefficient).

[L3]

$\mathbb{R}$ is a field, so a product of two nonzero reals is nonzero, and $-x = 0$ only for $x = 0$ (Field, The reals form a totally ordered field).

[L4]

The order on $\mathbb{Z}$ is total and compatible with addition (The integers form a totally ordered ring, Order on the integers).

Proof

technique · direct

1.1

By [L1] $f$ vanishes at every index below $p$ and $g$ at every index below $q$ , so by [L2] $(fg)(k) = 0$ for every $k < p + q$ .

L1L2

1.2

If $(i,j)$ satisfies $i + j = p+q$ and $f(i)g(j) \ne 0$ then $i \ge p$ and $j \ge q$ by [L1], and $i + j = p + q$ then forces $i = p$ and $j = q$ ; hence $(fg)(p+q) = f(p)g(q) = \operatorname{lc}(f)\operatorname{lc}(g)$ , which is nonzero by [L3].

L1L2L3L4

1.3

$(-f)(k) = -f(k)$ for every $k$ , so $-f$ vanishes exactly where $f$ does; by [L1] and [L3] this gives $-f \ne 0_K$ , $v(-f) = p$ and $\operatorname{lc}(-f) = -\operatorname{lc}(f) \ne 0$ .

L1L2L3

1.4

Suppose $p < q$ . For $k < p$ both $f(k) = 0$ and $g(k) = 0$ , so $(f+g)(k) = 0$ ; and $g(p) = 0$ because $p < q$ , so $(f+g)(p) = \operatorname{lc}(f) \ne 0$ . By [L1], $f + g \ne 0_K$ with $v(f+g) = p$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f)$ .

L1L2L4

1.5

Suppose $p = q$ and $\operatorname{lc}(f) + \operatorname{lc}(g) \ne 0$ . For $k < p$ both terms vanish, so $(f+g)(k) = 0$ ; and $(f+g)(p) = \operatorname{lc}(f) + \operatorname{lc}(g) \ne 0$ . By [L1], $f+g \ne 0_K$ , $v(f+g) = p$ and $\operatorname{lc}(f+g) = \operatorname{lc}(f) + \operatorname{lc}(g)$ .

L1L2

1.6

For $k < \min\{p,q\}$ one has $f(k) = g(k) = 0$ , hence $(f+g)(k) = 0$ ; so if $f + g \ne 0_K$ then its valuation, being the least index at which it is nonzero, satisfies $v(f+g) \ge \min\{p,q\}$ .

L1L2L4

2.1

By [step 1.1] $fg$ vanishes at every index below $p+q$ and by [step 1.2] it is nonzero at $p+q$ ; so by [L1] $fg \ne 0_K$ , $v(fg) = p + q$ and $\operatorname{lc}(fg) = \operatorname{lc}(f)\operatorname{lc}(g)$ . Since $f$ and $g$ were arbitrary nonzero elements, no product of nonzero elements of $K$ is zero.

step 1.1step 1.2L1

3.1

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].

step 1.3step 1.4step 1.5step 1.6step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

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

Valuation (algebra) (Wikipedia) (standard reference, not scraped)
Hahn series (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)

Valuation and leading coefficient in R((t−1))\mathbb{R}((t^{-1}))R((t−1)): v(fg)=v(f)+v(g)v(fg) = v(f) + v(g)v(fg)=v(f)+v(g), and the behaviour of vvv under sums