LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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 $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums

Statement

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

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

Facts & Assumptions

Given: $f, g \in K$ with $f \neq 0_{K}$ and $g \neq 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)) = lc (h) \neq 0$ ; conversely, if $h (k) = 0$ for all $k < r$ and $h (r) \neq 0$ then $h \neq 0_{K}$ , $v (h) = r$ and $lc (h) = h (r)$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$(f + g) (k) = f (k) + g (k)$ and $(f g) (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 $f g$ vanishes at every index below $m + n$ ( $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below, The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L3]

$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 $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] $(f g) (k) = 0$ for every $k < p + q$ .

L1L2

1.2

If $(i, j)$ satisfies $i + j = p + q$ and $f (i) g (j) \neq 0$ then $i \geq p$ and $j \geq q$ by [L1], and $i + j = p + q$ then forces $i = p$ and $j = q$ ; hence $(f g) (p + q) = f (p) g (q) = lc (f) 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 \neq 0_{K}$ , $v (- f) = p$ and $lc (- f) = - lc (f) \neq 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) = lc (f) \neq 0$ . By [L1], $f + g \neq 0_{K}$ with $v (f + g) = p$ and $lc (f + g) = lc (f)$ .

L1L2L4

1.5

Suppose $p = q$ and $lc (f) + lc (g) \neq 0$ . For $k < p$ both terms vanish, so $(f + g) (k) = 0$ ; and $(f + g) (p) = lc (f) + lc (g) \neq 0$ . By [L1], $f + g \neq 0_{K}$ , $v (f + g) = p$ and $lc (f + g) = lc (f) + 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 \neq 0_{K}$ then its valuation, being the least index at which it is nonzero, satisfies $v (f + g) \geq \min {p, q}$ .

L1L2L4

2.1

By [step 1.1] $f g$ vanishes at every index below $p + q$ and by [step 1.2] it is nonzero at $p + q$ ; so by [L1] $f g \neq 0_{K}$ , $v (f g) = p + q$ and $lc (f g) = lc (f) 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 · two levels

28 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

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))R((t−1)): v(fg)=v(f)+v(g)v(fg)=v(f)+v(g), and the behaviour of vv under sums