TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.1

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]$ .

givenL1L2L5

1.2

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

L6L7algebra

2.1

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.

step 1.2L1L2L4algebra

2.2

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}$ .

step 1.1L3L4

3.1

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.

step 2.2step 1.2L3

4.1

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}$ .

step 3.1step 2.1L2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 105 results over 19 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

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)