TheoremStatement: AI-adaptedProof: 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.

Over a named splitting field in characteristic zero, repeated characteristic roots give polynomial-times-exponential closed forms

Statement

Let $K$ be a field of characteristic zero, let $(a_{n})_{n \geq 0}$ satisfy an order- $d$ recurrence from zero, and let $E / K$ be a splitting field of its characteristic polynomial. If

$χ (t) = \prod_{i = 1}^{s} (t - λ_{i})^{m_{i}}$

in $E [t]$ , with distinct roots $λ_{i}$ , then there are unique polynomials $p_{i} \in E [z]$ with $\deg p_{i} < m_{i}$ such that

$a_{n} = \sum_{i = 1}^{s} p_{i} (n) λ_{i}^{n} (n \geq 0) .$

Conversely, every sequence of this form satisfies the recurrence whose characteristic polynomial is the displayed product. Equality is in $E$ , and no identification with $R$ or $C$ is assumed.

Facts & Assumptions

Given: A characteristic-zero field $K$ , a sequence satisfying a recurrence from zero, a named splitting field $E / K$ , and the displayed factorisation of its characteristic polynomial.

[L1]

A recurrence from zero has a proper rational generating function with its reciprocal denominator (A coefficient sequence is eventually linearly recurrent if and only if its formal generating function is rational).

[L2]

The factorisation $χ (t) = \prod_{i} (t - λ_{i})^{m_{i}}$ corresponds to $Q (x) = \prod_{i} (1 - λ_{i} x)^{m_{i}}$ (Reciprocal-root convention: $χ (t) = \prod_{i} (t - λ_{i})^{m_{i}}$ corresponds to $Q (x) = \prod_{i} (1 - λ_{i} x)^{m_{i}}$ ).

[L3]

A proper fraction with that split denominator has a unique expansion $\sum_{i, j} b_{i j} (1 - λ_{i} x)^{- j}$ (A proper rational function with split denominator has a unique repeated-pole partial-fraction expansion).

[L4]

Formally, $[x^{n}] (1 - λ x)^{- j} = (\binom{n + j - 1}{j - 1}) λ^{n}$ (Repeated poles expand formally as $(1 - λ x)^{- j} = \sum_{n \geq 0} (\binom{n + j - 1}{j - 1}) λ^{n} x^{n}$ ).

[L5]

A splitting field is generated by the roots over the base field, and repeated factors record their multiplicities (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[L6]

Characteristic zero means that no positive natural multiple of the field identity is zero (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise).

[L7]

The binomial coefficient satisfies $(\binom{n}{k}) k! = n^{\underline{k}}$ when $k \leq n$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ ).

Proof

technique · direct

1.1givenL1L2L5

By [L1] the generating function is $P / Q$ with $P = 0$ or $\deg P < d$ , and [L2] identifies $Q$ with the split product $\prod_{i} (1 - λ_{i} x)^{m_{i}}$ in $E [x]$ .

1.2L6L7algebra

By [L6], every positive factorial is nonzero and hence invertible in $E$ . For $1 \leq j \leq m$ put $q_{j} (z) = ((j - 1)!)^{- 1} (z + 1) (z + 2) \dots (z + j - 1) \in E [z]$ , the product being empty for $j = 1$ , so $q_{1} = 1$ . Each $q_{j}$ has degree $j - 1$ and leading coefficient $((j - 1)!)^{- 1} \neq 0$ , and for every natural $n$ the identity $(\binom{n + j - 1}{j - 1}) (j - 1)! = (n + j - 1)^{\underline{j - 1}} = (n + 1) \dots (n + j - 1)$ from [L7] gives $q_{j} (n) = (\binom{n + j - 1}{j - 1})$ . The degrees $0, \dots, m - 1$ are distinct, so triangular elimination makes $q_{1}, \dots, q_{m}$ a basis of the polynomials in $E [z]$ of degree below $m$ .

2.1step 1.2L1L2L4algebra

Conversely, expand each $p_{i}$ in the binomial-polynomial basis from step 1.2. Then [L4] shows that the generating function of $p_{i} (n) λ_{i}^{n}$ has denominator dividing $(1 - λ_{i} x)^{m_{i}}$ ; summing gives a rational function with denominator dividing $Q$ , so [L1] gives the recurrence with characteristic polynomial dividing the displayed product. Multiplying by any missing factors gives the displayed order- $d$ recurrence itself.

2.2step 1.1L3L4

Apply [L3] and then [L4] to obtain $a_{n} = \sum_{i = 1}^{s} \sum_{j = 1}^{m_{i}} b_{i j} (\binom{n + j - 1}{j - 1}) λ_{i}^{n}$ .

3.1step 2.2step 1.2L3

Step 1.2 rewrites each coefficient $(\binom{n + j - 1}{j - 1})$ as $q_{j} (n)$ , so grouping the terms of step 2.2 with the same $i$ gives $a_{n} = \sum_{i} p_{i} (n) λ_{i}^{n}$ with $p_{i} = \sum_{j = 1}^{m_{i}} b_{i j} q_{j}$ , a polynomial in $E [z]$ of degree below $m_{i}$ . Uniqueness follows from the uniqueness in [L3], the basis property in step 1.2, and coefficient extensionality.

4.1step 3.1step 2.1L2∎

Steps 3.1 and 2.1 prove both directions, including repeated roots and the case of one root. The condition $c_{d} \neq 0$ in the recurrence excludes zero among the $λ_{i}$ .

Depends on

Used by

Dependency tree · two levels

45 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., Theorem 4.1.1 (standard reference, not scraped)
B. E. Sagan, Combinatorics: The Art of Counting, Theorem 3.7.1 (standard reference, not scraped)
M. Waldschmidt, Linear Recurrence Sequences VI, slides 19-28 (standard reference, not scraped)