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

Negative binomial series: $(1 - x)^{- m} = \sum_{n \geq 0} (\binom{m + n - 1}{n}) x^{n}$ for $m \geq 1$

Example

For every commutative ring $R$ and integer $m \geq 1$ ,

$(1 - x)^{- m} = \sum_{n \geq 0} (\binom{m + n - 1}{n}) x^{n} .$

The binomial coefficient acts in $R$ by repeated addition of $1$ . When $R$ is a commutative $Q$ -algebra, this repeated inverse power agrees with the formal binomial power of Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

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

[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]

In a commutative $Q$ -algebra, formal $\exp$ and $\log$ are inverse group homomorphisms on $x R ⟦ x ⟧$ and $1 + x R ⟦ x ⟧$ , and for $u \in x R ⟦ x ⟧$ and $c, d \in R$ the exponent-addition and exponent-multiplication laws hold (Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws).

[F4]

For $m \geq 1$ , the weak compositions of $n$ into $m$ parts are counted by $(\binom{n + m - 1}{m - 1})$ (For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ ).

[F5]

$(\binom{n}{k})$ is the number of $k$ -element subsets of an $n$ -element set (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

Verification

technique · count the product convolution

1.1

Put $s = \sum_{j \geq 0} x^{j}$ . Its constant coefficient in $(1 - x) s$ is $1$ , and every positive-degree coefficient is $1 - 1 = 0$ , so extensionality and inverse uniqueness give $s = (1 - x)^{- 1}$ . Hence $(1 - x)^{- m}$ is the product of $m$ copies of $s$ over every commutative ring. Over a commutative $Q$ -algebra, the formal exponent law gives the same series.

givenF1F2F3

2.1

The coefficient of $x^{n}$ in this product is the number of $m$ -tuples $(j_{1}, \dots, j_{m})$ of nonnegative integers with sum $n$ . The stars-and-bars count makes this $(\binom{n + m - 1}{m - 1}) = (\binom{m + n - 1}{n})$ . At $n = 0$ the unique tuple is all zero, giving coefficient $1$ .

step 1.1givenF4F5

3.1

Coefficient extensionality now gives the asserted series identity for every $m \geq 1$ . When $m = 1$ the coefficient is $(\binom{n}{n}) = 1$ , recovering the series $s$ from step 1.1; step 2.1 already checks $n = 0$ .

step 1.1step 2.1givenF2∎

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: 88 results over 24 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)

Negative binomial series: (1−x)−m=∑n≥0(m+n−1n)xn(1−x)−m=∑n≥0​(nm+n−1​)xn for m≥1m≥1