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

$R ⟦ x ⟧$ is complete in the $x$ -adic topology and $R [x]$ is dense by truncation

Statement

Every $x$ -adically Cauchy sequence in $R ⟦ x ⟧$ has a unique $x$ -adic limit. For every $f \in R ⟦ x ⟧$ , its truncations

$f_{< N} : = \sum_{n < N} [x^{n}] f x^{n} \in R [x]$

converge $x$ -adically to $f$ . Thus $R ⟦ x ⟧$ is $x$ -adically complete and the embedded polynomial ring is dense, including when $R$ is the zero ring.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

An $x$ -adically Cauchy sequence eventually agrees pairwise modulo every $x^{N}$ , and convergence means eventual agreement with the limit modulo every $x^{N}$ (Order of a formal series, congruence modulo $x^{N}$ , and the $x$ -adic notions of convergence and Cauchy sequence).

[F2]

The coefficientwise polynomial inclusion into formal power series is an injective unital ring homomorphism (Cauchy multiplication makes $R ⟦ x ⟧$ a commutative ring containing $R [x]$ as the finitely supported subring).

[F3]

Two formal series are equal if and only if all their coefficients are equal (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

Proof

technique · stabilize coefficients

1.1

Let $(f_{j})$ be Cauchy. For each $n$ , use the Cauchy condition with $N = n + 1$ : the coefficient $[x^{n}] f_{j}$ is eventually constant. Define $[x^{n}] f$ to be that eventual value. Given $N$ , choose a common Cauchy index for the first $N$ coefficients; then $f_{j} \equiv f (m o d x^{N})$ thereafter, so $f_{j} \to f$ .

givenF1

1.2

The truncation $f_{< N}$ is finitely supported, hence belongs to the embedded $R [x]$ , and it agrees with $f$ in every degree below $N$ . Therefore $f_{< N} \to f$ ; this includes a constant or zero series and remains true in the zero ring.

givenF2

2.1

If both $f$ and $g$ are limits, then for each $N$ their first $N$ coefficients agree with the same sufficiently late $f_{j}$ . Thus every coefficient of $f$ and $g$ agrees, so $f = g$ by extensionality.

step 1.1givenF3

3.1

Existence and uniqueness are steps 1.1 and 2.1, and density is step 1.2.

step 1.1step 2.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

R⟦x⟧R[[x]] is complete in the xx-adic topology and R[x]R[x] is dense by truncation