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

Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra

Statement

Let $R$ be a commutative $Q$ -algebra, $u \in x R ⟦ x ⟧$ , and $k \geq 1$ . There is a unique $v \in 1 + x R ⟦ x ⟧$ such that

$v^{k} = 1 + u,$

namely $v = (1 + u)^{1 / k}$ . When $u = 0$ , this unique root is $1$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

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

Proof

technique · apply the formal logarithm

1.1

The power law gives $((1 + u)^{1 / k})^{k} = (1 + u)^{1} = 1 + u$ , so the stated series is a root with constant coefficient $1$ .

givenF1

1.2

If $v \in 1 + x R ⟦ x ⟧$ and $v^{k} = 1 + u$ , the logarithm addition law gives $k \log v = \log (1 + u)$ . Since $k$ is invertible in a $Q$ -algebra, $\log v = (1 / k) \log (1 + u)$ ; applying $\exp$ gives $v = (1 + u)^{1 / k}$ . This proves uniqueness.

givenF1

2.1

For $u = 0$ , the construction is $\exp (0) = 1$ , and step 1.2 excludes any other constant-one root.

step 1.1step 1.2givenF1∎

Depends on

Used by

The constant-one square root of 1-4x and its first coefficients Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 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)

Every 1+u1+u with u∈xR⟦x⟧u∈xR[[x]] has a unique kkth root with constant coefficient 11 in a commutative QQ-algebra