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

Formal order is non-Archimedean under sums and additive under products over a domain

Statement

For formal series over a commutative ring,

${ord}_{x} (f + g) \geq \min ({ord}_{x} f, {ord}_{x} g),$

and

${ord}_{x} (f g) \geq {ord}_{x} f + {ord}_{x} g .$

If $f, g \neq 0$ have orders $p, q$ and $[x^{p}] f [x^{q}] g \neq 0$ , then equality holds in the product inequality and $[x^{p + q}] (f g) = [x^{p}] f [x^{q}] g$ . Consequently, over an integral domain,

${ord}_{x} (f g) = {ord}_{x} f + {ord}_{x} g$

with the $+ \infty$ convention, and $R ⟦ x ⟧$ is an integral domain whenever $R$ is.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

The formal order of a nonzero series is its least nonzero coefficient index, and ${ord}_{x} (0) = + \infty$ (Order of a formal series, congruence modulo $x^{N}$ , and the $x$ -adic notions of convergence and Cauchy sequence).

[F2]

The product on $R ⟦ x ⟧$ is the Cauchy product (Cauchy multiplication makes $R ⟦ x ⟧$ a commutative ring containing $R [x]$ as the finitely supported subring).

[F3]

An integral domain is a commutative ring with $1 \neq 0$ and no zero divisors (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors).

Proof

technique · inspect the first possible nonzero coefficient

1.1

Below the smaller of the two orders, both summand coefficients vanish, so the sum coefficient vanishes. This proves the sum inequality; if one order is strictly smaller, its leading coefficient cannot be cancelled by the other series.

givenF1

1.2

If $p = {ord}_{x} f$ and $q = {ord}_{x} g$ are finite, every convolution summand in degree below $p + q$ has one zero factor. In degree $p + q$ , only the pair $(p, q)$ can be nonzero, so the coefficient there is $[x^{p}] f [x^{q}] g$ . If either series is zero, the stated inequality follows from the $+ \infty$ conventions.

givenF1F2

2.1

Over a domain the product of the two nonzero leading coefficients is nonzero, so step 1.2 gives exact additivity. In particular two nonzero series have a nonzero product; $R ⟦ x ⟧$ also has $1 \neq 0$ because its constant coefficients are those of $R$ .

step 1.2givenF3

3.1

Steps 1.1-2.1 prove all order laws and the domain conclusion, including zero factors.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

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