TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws

Statement

In a commutative $Q$ -algebra $R$ , for $u, v \in x R ⟦ x ⟧$ and $c, d \in R$ ,

$\exp (u + v) = \exp (u) \exp (v),$

$\log ((1 + u) (1 + v)) = \log (1 + u) + \log (1 + v),$

and $\exp : x R ⟦ x ⟧ \to 1 + x R ⟦ x ⟧$ and $\log : 1 + x R ⟦ x ⟧ \to x R ⟦ x ⟧$ are inverse group homomorphisms. Consequently,

$(1 + u)^{c + d} = (1 + u)^{c} (1 + u)^{d}, ((1 + u)^{c})^{d} = (1 + u)^{c d},$

and

$(1 + u)^{c} = \sum_{n \geq 0} \frac{c (c - 1) \dots (c - n + 1)}{n!} u^{n},$

where the numerator is the empty product $1$ at $n = 0$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

Formal exponential and logarithm are $\exp (u) = \sum_{n \geq 0} u^{n} / n!$ and $\log (1 + u) = \sum_{n \geq 1} (- 1)^{n - 1} u^{n} / n$ (Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra).

[F2]

Formal binomial powers are defined by $(1 + u)^{c} = \exp (c \log (1 + u))$ (Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra).

[F3]

The formal derivative is additive, obeys the product rule, and satisfies $D (f^{m}) = m f^{m - 1} D f$ for $m \geq 1$ while $D (1) = 0$ (Formal differentiation is linear and satisfies product, power, quotient, chain, and coefficient-recovery laws).

[F4]

A summable family may be bijectively reindexed or partitioned and regrouped without changing its sum (Summable formal families may be regrouped and rearranged, distribute over multiplication, and have well-defined locally finite products).

Proof

technique · finite coefficient convolution and formal differentiation

1.1

Expanding the product and regrouping in each degree gives $\exp (u) \exp (v) = \sum_{n \geq 0} (u + v)^{n} / n!$ by the finite binomial identity, so the exponential addition law holds.

givenF1F4

1.2

Termwise differentiation gives $D \exp (u) = (\exp u) D u$ and $D \log (1 + u) = (1 + u)^{- 1} D u$ . Hence $D (\log (\exp u) - u) = 0$ , and its constant coefficient is $0$ , so $\log (\exp u) = u$ . For $z = 1 + u$ and $y = \exp (\log z)$ , the same formulas give $D (y z^{- 1}) = 0$ and $(y z^{- 1}) (0) = 1$ , so $y = z$ . Here a zero derivative forces every positive-degree coefficient to vanish because every positive integer is invertible in a $Q$ -algebra.

givenF1F3

1.3

In an independent indeterminate $z$ , let $B_{c} (z)$ denote the displayed generalized-binomial series. Direct coefficient algebra gives $B_{c} (0) = 1$ and $(1 + z) D_{z} B_{c} (z) = c B_{c} (z)$ . The formally defined $(1 + z)^{c}$ has the same constant coefficient and differential equation. Recursively comparing coefficients, where $n$ is invertible for $n \geq 1$ , makes the two series equal; admissible substitution $z = u$ gives the asserted formula.

givenF2F3

2.1

Step 1.2 and the exponential addition law give $\exp (\log (1 + u) + \log (1 + v)) = (1 + u) (1 + v)$ ; applying $\log$ gives the logarithm addition law. The two power laws follow by substituting their definition and applying the exponential and logarithm laws.

step 1.1step 1.2givenF2

3.1

Steps 1.1-2.1 prove the inverse homomorphisms, both power laws, and the coefficient formula, including $u = 0$ , $c = 0$ , and $n = 0$ .

step 1.1step 1.2step 2.1step 1.3∎

Depends on

Used by

Dependency tree · two levels

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

Formal exp⁡exp and log⁡log are inverse homomorphisms and formal binomial powers obey the expected addition laws