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

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

Example

In $Q ⟦ x ⟧$ , the unique square root of $1 - 4 x$ with constant coefficient $1$ begins

$\sqrt{1 - 4 x} = 1 - 2 x - 2 x^{2} - 4 x^{3} - 10 x^{4} - 28 x^{5} + O (x^{6}),$

where $O (x^{6})$ means a series of order at least $6$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

For a commutative $Q$ -algebra $R$ , $u \in x R ⟦ x ⟧$ , and $k \geq 1$ , $1 + u$ has the unique root in $1 + x R ⟦ x ⟧$ , namely $(1 + u)^{1 / k}$ (Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra).

[F2]

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

[F3]

The formal order of a nonzero series is its least nonzero coefficient index, and ${ord}_{x} (0) = + \infty$ (Order of a formal series, congruence modulo $x^{N}$ , and the $x$ -adic notions of convergence and Cauchy sequence).

Verification

technique · square the truncation

1.1

Let $q = 1 - 2 x - 2 x^{2} - 4 x^{3} - 10 x^{4} - 28 x^{5}$ . Cauchy convolution gives $[x^{0}] q^{2} = 1$ , $[x] q^{2} = - 4$ , and coefficients $4 - 4$ , $- 8 + 8$ , $- 20 + 16 + 4$ , and $- 56 + 40 + 16$ , all $0$ , in degrees $2, 3, 4, 5$ respectively. Hence $q^{2} \equiv 1 - 4 x (m o d x^{6})$ .

givenF2F3

2.1

The unique constant-one square root has coefficients determined successively by the equation $v^{2} = 1 - 4 x$ because its unknown degree- $n$ coefficient occurs as $2 [x^{n}] v$ . Step 1.1 therefore gives its coefficients through degree $5$ .

step 1.1givenF1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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 constant-one square root of 1−4x1−4x and its first coefficients