ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck 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.

The formal geometric identity $(1 - x)^{- 1} = \sum_{n \geq 0} x^{n}$ holds over every commutative ring

Example

In $R ⟦ x ⟧$ , for every commutative ring $R$ ,

$(1 - x)^{- 1} = 1 + x + x^{2} + x^{3} + \dots .$

This includes the zero ring.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

Product coefficients satisfy $[x^{n}] (f g) = \sum_{i = 0}^{n} [x^{i}] f [x^{n - i}] g$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[F2]

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).

[F3]

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).

Verification

technique · multiply and compare coefficients

1.1

The series $s = \sum_{n \geq 0} x^{n}$ has every coefficient equal to $1$ . The constant coefficient of $(1 - x) s$ is $1$ , and for $n \geq 1$ its coefficient is $[x^{n}] s - [x^{n - 1}] s = 1 - 1 = 0$ .

givenF1

2.1

Thus $(1 - x) s = 1$ by coefficient extensionality. Since $1 - x$ has unit constant coefficient $1$ , its inverse is unique, so $s = (1 - x)^{- 1}$ . In the zero ring both sides are the unique series.

step 1.1givenF2F3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

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

The formal geometric identity (1−x)−1=∑n≥0xn(1−x)−1=∑n≥0​xn holds over every commutative ring