ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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 repeated pole $(1 - 2 x)^{- 2}$ produces the sequence $(n + 1) 2^{n}$

Example

In $Q ⟦ x ⟧$ ,

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

The coefficient sequence $a_{n} = (n + 1) 2^{n}$ satisfies

$a_{n + 2} - 4 a_{n + 1} + 4 a_{n} = 0,$

whose characteristic polynomial is $(t - 2)^{2}$ . Thus the root $2$ of multiplicity two produces a polynomial factor of degree one.

Facts & Assumptions

Given: The repeated pole $(1 - 2 x)^{- 2}$ .

[L1]

The repeated-pole expansion is $(1 - λ x)^{- j} = \sum_{n \geq 0} (\binom{n + j - 1}{j - 1}) λ^{n} x^{n}$ (Repeated poles expand formally as $(1 - λ x)^{- j} = \sum_{n \geq 0} (\binom{n + j - 1}{j - 1}) λ^{n} x^{n}$ ).

[L2]

A factor $(t - λ)^{m}$ in the characteristic polynomial corresponds to $(1 - λ x)^{m}$ in the reciprocal denominator (Reciprocal-root convention: $χ (t) = \prod_{i} (t - λ_{i})^{m_{i}}$ corresponds to $Q (x) = \prod_{i} (1 - λ_{i} x)^{m_{i}}$ ).

[L3]

The characteristic polynomial of $a_{n + 2} + c_{1} a_{n + 1} + c_{2} a_{n} = 0$ is $t^{2} + c_{1} t + c_{2}$ (Constant-coefficient linear recurrences, their starting index and their characteristic polynomial).

Verification

technique · direct calculation

1.1givenL1algebra

Apply [L1] with $j = 2$ and $λ = 2$ ; since $(\binom{n + 1}{1}) = n + 1$ , this gives the displayed series.

1.2algebra

Direct substitution gives $a_{n + 2} - 4 a_{n + 1} + 4 a_{n} = 2^{n} (4 n + 12 - 8 n - 16 + 4 n + 4) = 0$ .

2.1step 1.2L2L3algebra∎

By [L3], the recurrence polynomial is $t^{2} - 4 t + 4 = (t - 2)^{2}$ , and [L2] matches it to the given double pole.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

B. E. Sagan, Combinatorics: The Art of Counting, Section 3.7 (standard reference, not scraped)

The repeated pole (1−2x)−2(1−2x)−2 produces the sequence (n+1)2n(n+1)2n