ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 Lucas generating function and its two-root closed form

Example

With $ϕ = (1 + \sqrt{5}) / 2$ and $\hat{ϕ} = (1 - \sqrt{5}) / 2$ , the Lucas sequence satisfies

$\sum_{n \geq 0} L_{n} x^{n} = \frac{2 - x}{1 - x - x^{2}}$

in $Q ⟦ x ⟧$ , and

$L_{n} = ϕ^{n} + {\hat{ϕ}}^{n}$

in $Q (\sqrt{5})$ for every $n \geq 0$ .

Facts & Assumptions

Given: The Lucas initial values and recurrence.

[L1]

The Lucas sequence satisfies $L_{0} = 2$ , $L_{1} = 1$ , and $L_{n + 2} = L_{n + 1} + L_{n}$ (The Fibonacci sequence $F_{0} = 0, F_{1} = 1$ and Lucas sequence $L_{0} = 2, L_{1} = 1$ ).

[L2]

A recurrence beginning at zero has a rational generating function whose numerator is obtained by multiplying by its reciprocal denominator (A coefficient sequence is eventually linearly recurrent if and only if its formal generating function is rational).

[L3]

Distinct roots of a characteristic polynomial give a unique pure-exponential closed form over a characteristic-zero splitting field (Over a named splitting field in characteristic zero, repeated characteristic roots give polynomial-times-exponential closed forms).

Verification

technique · direct

1.1givenL1L2algebra

For $L (x) = \sum_{n \geq 0} L_{n} x^{n}$ , [L1] gives $(1 - x - x^{2}) L (x) = L_{0} + (L_{1} - L_{0}) x = 2 - x$ , so [L2] proves the generating-function formula.

1.2L3algebra

Since $t^{2} - t - 1 = (t - ϕ) (t - \hat{ϕ})$ , [L3] gives $L_{n} = A ϕ^{n} + B {\hat{ϕ}}^{n}$ .

2.1step 1.2L1algebra

The initial equations $A + B = 2$ and $A ϕ + B \hat{ϕ} = 1$ have the solution $A = B = 1$ , because $ϕ + \hat{ϕ} = 1$ .

3.1step 2.1∎

Substitution in step 2.1 proves the displayed closed form for all $n \geq 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

R. P. Stanley, Enumerative Combinatorics, vol. 1, 2nd ed., Example 4.7.16 (standard reference, not scraped)