TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

$K ⟦ x ⟧$ embeds in $K ((x))$ as the nonnegative-order subring; every nonzero Laurent series is uniquely $x^{v_{x} (h)} u$ with $u \in K ⟦ x ⟧^{\times}$ and inverse $x^{- v_{x} (h)} u^{- 1}$

Statement

For every field $K$ , extending a power series by zero at negative exponents gives an injective unital ring homomorphism

$K ⟦ x ⟧ ↪ K ((x))$

whose image is ${0} \cup {h : v_{x} (h) \geq 0}$ . Every nonzero $h \in K ((x))$ has a unique factorisation

$h = x^{v_{x} (h)} u, u \in K ⟦ x ⟧^{\times},$

and

$h^{- 1} = x^{- v_{x} (h)} u^{- 1} .$

For $K = R$ , the substitution $x^{n} \mapsto t^{- n}$ identifies this description with the published real Laurent-series construction.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

Formal Laurent series have support bounded below, coefficientwise addition, finite convolution in each degree, least exponent $v_{x}$ , termwise derivative, and residue ${res}_{x} (f) = [x^{- 1}] f$ (Formal Laurent series $K ((x))$ , their order, derivative, and residue).

[F2]

A formal power series is a unit exactly when its constant coefficient is a unit (A formal power series is a unit exactly when its constant coefficient is a unit).

[F3]

Every nonzero published real Laurent series has a multiplicative inverse constructed from its leading term ( $R ((t^{- 1}))$ is a field: every nonzero formal Laurent series is invertible).

[F4]

For nonzero published real Laurent series, $v (f g) = v (f) + v (g)$ and the leading coefficients multiply (Valuation and leading coefficient in $R ((t^{- 1}))$ : $v (f g) = v (f) + v (g)$ , and the behaviour of $v$ under sums).

Proof

technique · extend and shift coefficient functions

1.1

Extending coefficients by zero at negative integers preserves addition, $1$ , and every finite convolution, and is injective. Its nonzero image has nonnegative least exponent; conversely every Laurent series of nonnegative order already has no negative coefficient and so comes from a unique power series.

givenF1

1.2

Let $m = v_{x} (h)$ . Define $u = x^{- m} h$ . Then $u \in K ⟦ x ⟧$ and its constant coefficient is the nonzero leading coefficient of $h$ , so $u$ is a unit. This gives $h = x^{m} u$ and $x^{- m} u^{- 1}$ is directly a two-sided inverse. If $h = x^{a} v = x^{b} u$ with the two final factors constant-term units, least exponents give $a = b = m$ and coefficient extensionality gives $u = v$ .

givenF1F2

2.1

Over $R$ , sending coefficient $a_{n} x^{n}$ to $a_{n} t^{- n}$ preserves finite convolution. The least $x$ -exponent becomes the published least $t^{- 1}$ -exponent, so the order, factorisation, unit, and inverse formulas agree with the cited real theorem and valuation lemma.

step 1.1step 1.2givenF3F4

3.1

Steps 1.1-2.1 prove the embedding, image, unique factorisation, inverse formula, and real-coordinate dictionary.

step 1.1step 1.2step 2.1∎

Depends on

Used by

x has no multiplicative inverse in R llbracket x rrbracket although it is invertible in K((x)) when R=K is a field Counterexample

Dependency tree · next 3 levels

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

Benjamin Sambale, An Invitation to Formal Power Series (standard reference, not scraped)

K⟦x⟧K[[x]] embeds in K((x))K((x)) as the nonnegative-order subring; every nonzero Laurent series is uniquely xvx(h)uxvx​(h)u with u∈K⟦x⟧×u∈K[[x]]× and inverse x−vx(h)u−1x−vx​(h)u−1