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

$R ((t^{- 1}))$ is a field: every nonzero formal Laurent series is invertible

Statement

$K = R ((t^{- 1}))$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient) is a field (Field): it is a commutative ring with $1_{K} \neq 0_{K}$ , and every $f \in K$ with $f \neq 0_{K}$ has a multiplicative inverse in $K$ .

Explicitly, if $p = v (f)$ and $c = lc (f)$ , then $f = ι (c) t^{- p} (1_{K} - u)$ for the element $u \in K$ given by $u (j) = - c^{- 1} f (p + j)$ for $j \geq 1$ and $u (j) = 0$ for $j \leq 0$ , and $f^{- 1} = ι (c^{- 1}) t^{p} g$ , where $g \in K$ vanishes at every index $< 0$ and is given at $k \geq 0$ by $g (k) = \sum_{n = 0}^{k} (u^{n}) (k)$ .

Scratch work

The identity behind the construction is the geometric series $(1 - u)^{- 1} = 1 + u + u^{2} + \dots$ . It cannot be used as written, because $K$ has no notion of an infinite sum. What replaces it is the observation that $u^{n}$ vanishes at every index below $n$ , so at any single index $k$ only the terms $n \leq k$ can contribute; the displayed formula for $g (k)$ is that finite truncation, and the support of the result is bounded below because every $u^{n}$ vanishes below $0$ .

Facts & Assumptions

Given: A nonzero $f \in K$ ; write $p : = v (f) \in Z$ and $c : = lc (f) \in R ∖ {0}$ , so that $f (k) = 0$ for every $k < p$ and $f (p) = c$ .

[L1]

$K$ is the set of functions $Z \to R$ whose support is bounded below; $t^{- a}$ is $1$ at index $a$ and $0$ elsewhere; $ι (c)$ is $c$ at index $0$ and $0$ elsewhere; for nonzero $h \in K$ one has $h (k) = 0$ for $k < v (h)$ and $h (v (h)) = lc (h) \neq 0$ (The formal Laurent series $R ((t^{- 1}))$ : support bounded below, valuation, leading coefficient).

[L2]

$K$ is a commutative ring with identity $1_{K} \neq 0_{K}$ ; $(h_{1} h_{2}) (k) = \sum_{i + j = k} h_{1} (i) h_{2} (j)$ is a finite sum; if $h_{1}$ vanishes at every index $< a$ and $h_{2}$ at every index $< b$ then $h_{1} h_{2}$ vanishes at every index $< a + b$ ; $(t^{- a} h) (k) = h (k - a)$ and hence $t^{- a} t^{- b} = t^{- (a + b)}$ ; and $(ι (c) h) (k) = c h (k)$ ( $R ((t^{- 1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below).

[L3]

A product of two nonzero elements of $K$ is nonzero (Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums).

[L4]

$R$ is a field: every nonzero $c$ has an inverse $c^{- 1}$ with $c c^{- 1} = 1$ , and a finite sum of reals may be reordered and regrouped freely (Field, The reals form a totally ordered field).

[L5]

Recursion on $N$ : for a set $A$ , an element $a \in A$ and a function $F : A \to A$ there is a unique $Γ : N \to A$ with $Γ (0) = a$ and $Γ (σ (n)) = F (Γ (n))$ (The recursion theorem, The natural numbers $N$ (von Neumann)).

[L6]

Induction: a property holding at $0$ and inherited from $n$ to $σ (n)$ holds at every natural number (The principle of mathematical induction).

[L7]

A field is a commutative ring with $0 \neq 1$ in which multiplication restricted to the nonzero elements is an abelian group, that is, in which the nonzero elements are closed under multiplication and each has an inverse (Field).

Proof

technique · constructive

1.1

Define $u : Z \to R$ by $u (j) : = - c^{- 1} f (p + j)$ for $j \geq 1$ and $u (j) : = 0$ for $j \leq 0$ . Then $u$ vanishes at every index $< 1$ , so its support is bounded below and $u \in K$ .

givenL1L4construct

1.2

By [L5] with $A = K$ , $a = 1_{K}$ and $F (h) = h u$ there is a family $(u^{n})_{n \in N}$ in $K$ with $u^{0} = 1_{K}$ and $u^{σ (n)} = u^{n} u$ .

L2L5construct

2.1

For every $k \in Z$ , $(ι (c) t^{- p} (1_{K} - u)) (k) = c (1_{K} - u) (k - p)$ by [L2]; this is $0$ when $k < p$ because $1_{K} - u$ vanishes at every negative index, it is $c$ when $k = p$ , and it is $c \cdot (- u (k - p)) = c c^{- 1} f (k) = f (k)$ when $k > p$ . Comparing with $f (k) = 0$ for $k < p$ and $f (p) = c$ , we get $f = ι (c) t^{- p} (1_{K} - u)$ .

step 1.1givenL1L2L4

2.2

For every $n \in N$ , $u^{n}$ vanishes at every index $< n$ : at $n = 0$ this says $1_{K}$ vanishes at every negative index, which holds by [L1]; and if $u^{n}$ vanishes at every index $< n$ then, since $u$ vanishes at every index $< 1$ by [step 1.1], the product $u^{σ (n)} = u^{n} u$ vanishes at every index $< n + 1$ by [L2].

step 1.1step 1.2L1L2L6

3.1

Define $g : Z \to R$ by $g (k) : = \sum_{n = 0}^{k} (u^{n}) (k)$ for $k \geq 0$ and $g (k) : = 0$ for $k < 0$ ; each value is a finite sum of reals, and $g$ vanishes at every index $< 0$ , so $g \in K$ .

step 2.2L1L4construct

4.1

Fix $k \geq 1$ . In $(u g) (k) = \sum_{i + j = k} u (i) g (j)$ a term can be nonzero only when $i \geq 1$ and $j \geq 0$ , hence only for $1 \leq i \leq k$ and $j = k - i$ ; so $(u g) (k) = \sum_{i = 1}^{k} u (i) g (k - i) = \sum_{i = 1}^{k} u (i) \sum_{n = 0}^{k - i} (u^{n}) (k - i)$ .

step 1.1step 3.1L1L2

4.2

For $k \leq 0$ one has $(u g) (k) = 0$ , since $u$ vanishes at every index $< 1$ and $g$ at every index $< 0$ , so every pair $(i, j)$ with $i + j = k$ has $u (i) g (j) = 0$ .

step 1.1step 3.1L1L2

5.1

In the inner sum of [step 4.1] the terms with $k - i < n \leq k - 1$ vanish by [step 2.2], so the inner sum may be extended to $n = 0, \dots, k - 1$ without changing its value; interchanging the two finite sums gives $(u g) (k) = \sum_{n = 0}^{k - 1} \sum_{i = 1}^{k} u (i) (u^{n}) (k - i)$ .

step 2.2step 4.1L4

6.1

For each $n$ , $\sum_{i = 1}^{k} u (i) (u^{n}) (k - i) = \sum_{i + j = k} u (i) (u^{n}) (j) = (u u^{n}) (k) = (u^{σ (n)}) (k)$ , because a term of the full convolution can be nonzero only for $i \geq 1$ and $j \geq 0$ ; hence $(u g) (k) = \sum_{n = 0}^{k - 1} (u^{σ (n)}) (k) = \sum_{n = 1}^{k} (u^{n}) (k)$ for every $k \geq 1$ .

step 1.2step 2.2step 5.1L2

7.1

For $k \geq 1$ , $((1_{K} - u) g) (k) = g (k) - (u g) (k) = \sum_{n = 0}^{k} (u^{n}) (k) - \sum_{n = 1}^{k} (u^{n}) (k) = (u^{0}) (k) = 1_{K} (k)$ ; for $k = 0$ , $g (0) = (u^{0}) (0) = 1$ and $(u g) (0) = 0$ , so the value is $1 = 1_{K} (0)$ ; and for $k < 0$ both $g (k)$ and $(u g) (k)$ are $0$ , as is $1_{K} (k)$ . Hence $(1_{K} - u) g = 1_{K}$ .

step 3.1step 4.2step 6.1L1L2

8.1

Using [step 2.1], [L2] and $c c^{- 1} = 1$ , one computes $f \cdot (ι (c^{- 1}) t^{p} g) = ι (c) ι (c^{- 1}) t^{- p} t^{- (- p)} (1_{K} - u) g = 1_{K} \cdot 1_{K} \cdot 1_{K} = 1_{K}$ , so $ι (c^{- 1}) t^{p} g \in K$ is a multiplicative inverse of $f$ .

step 2.1step 7.1L2L4

9.1

$K$ is a commutative ring with $1_{K} \neq 0_{K}$ by [L2], its nonzero elements are closed under multiplication by [L3], and by [step 8.1] every nonzero element has an inverse; so $K$ satisfies the field axioms of [L7] and the construction is complete.

step 8.1L2L3L7discharge-construct∎

Remarks

Where support-boundedness is really used. Twice, and in different ways. It makes each coefficient of a product a finite sum, which is what lets $(u^{n}) (k)$ be spoken of at all; and it is what has to be re-established for the constructed inverse, which is why $g$ was defined to vanish at every negative index rather than found to. The verification that this definition is consistent with $(1_{K} - u) g = 1_{K}$ is [step 7.1], and it is exactly the point at which an infinite geometric series would have had to be summed.
The normalisation is forced, and that is why the recipe is explicit. Suppose $f = ι (c^{'}) t^{- p^{'}} (1_{K} - w)$ with $c^{'} \neq 0$ and $w$ vanishing at every index $\leq 0$ . Evaluating as in [step 2.1] gives $f (k) = c^{'} (1_{K} - w) (k - p^{'})$ , which is $0$ for $k < p^{'}$ and equals $c^{'}$ at $k = p^{'}$ ; so $p^{'} = v (f)$ and $c^{'} = lc (f)$ , and then $w (j) = - c^{' - 1} f (p^{'} + j)$ for $j \geq 1$ . The factorisation used in the proof is therefore the only one of its shape, and the formula for the inverse is a recipe rather than a choice.

Depends on

Used by

Cited to discharge well-definedness by The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient.

Dependency tree · two levels

26 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

Formal power series (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)

R((t−1))R((t−1)) is a field: every nonzero formal Laurent series is invertible