ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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 geometric series re-expanded about an arbitrary point of the unit disc

Example

For $∣ b ∣ < 1$ , $\frac{1}{1 - z} = \sum_{k = 0}^{\infty} \frac{(z - b)^{k}}{(1 - b)^{k + 1}} (∣ z - b ∣ < ∣ 1 - b ∣) .$ Thus the geometric sum re-expanded about $b$ has radius $∣ 1 - b ∣$ .

Facts & Assumptions

Given: A complex number $b$ with $∣ b ∣ < 1$ .

[L1]

A complex power-series sum re-expands about every interior point (A complex power-series sum re-expands about every interior point, at least to the distance from that point to the original boundary).

[L2]

If $L = {lim sup}_{k \to \infty} ∣ c_{k + 1} ∣^{1 / (k + 1)}$ , Cauchy–Hadamard gives radius $+ \infty$ for $L = 0$ , radius $1 / L$ for $0 < L < + \infty$ , and radius $0$ for $L = + \infty$ , with no boundary assertion (Cauchy-Hadamard for complex power series, including zero and infinite radius).

Verification

technique · direct

1.1

Rewrite $1 - z = (1 - b) (1 - (z - b) / (1 - b))$ ; since $b \neq 1$ , the finite geometric identity gives the displayed infinite series when $∣ (z - b) / (1 - b) ∣ < 1$ .

algebra

2.1

The coefficient modulus is $∣ 1 - b ∣^{- k - 1}$ , whose root limsup is $∣ 1 - b ∣^{- 1}$ , so [L2] gives radius $∣ 1 - b ∣$ .

step 1.1L2

3.1

The coefficients agree with the interior re-expansion guaranteed by [L1], and no assertion is made on its boundary circle.

step 1.1step 2.1L1∎

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: 61 results over 14 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

Power-series supplementary notes, Colby College (standard reference, not scraped)