LemmaStatement: AI-adaptedProof: 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 initial-value, recurrence-sequence, numerator and fixed-denominator rational-series spaces all have dimension $d$

Statement

Let $K$ be a field, let $d \geq 1$ , let $c_{1}, \dots, c_{d} \in K$ with $c_{d} \neq 0$ , and put $Q (x) = 1 + c_{1} x + \dots + c_{d} x^{d}$ . The following four $K$ -vector spaces are naturally linearly isomorphic:

the initial-value space $K^{d}$ ;
the space of sequences satisfying $a_{n + d} + c_{1} a_{n + d - 1} + \dots + c_{d} a_{n} = 0$ for every $n \geq 0$ ;
the space of polynomials $P$ with $P = 0$ or $\deg P < d$ ;
the space of formal series $P / Q$ with $P = 0$ or $\deg P < d$ .

Each space has dimension $d$ .

Facts & Assumptions

Given: A field $K$ , a positive order $d$ , coefficients $c_{1}, \dots, c_{d}$ with $c_{d} \neq 0$ , and $Q (x) = 1 + c_{1} x + \dots + c_{d} x^{d}$ .

[L1]

An order- $d$ recurrence from the start is $a_{n + d} + c_{1} a_{n + d - 1} + \dots + c_{d} a_{n} = 0$ for every $n \geq 0$ (Constant-coefficient linear recurrences, their starting index and their characteristic polynomial).

[L2]

A proper fixed-denominator series has the form $P / Q$ with $Q (0) = 1$ and either $P = 0$ or $\deg P < \deg Q$ (Rational formal power series, proper presentations and reduced denominators).

[L3]

Formal series are equal exactly when all their coefficients agree, and $[x^{n}] (Q F) = \sum_{i = 0}^{n} [x^{i}] Q [x^{n - i}] F$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[L4]

The standard unit vectors form a basis of $K^{d}$ , so $\dim_{K} K^{d} = d$ , including the zero-dimensional boundary (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

Proof

technique · direct

1.1givenL1construct

Given $(u_{0}, \dots, u_{d - 1}) \in K^{d}$ , set $a_{i} = u_{i}$ for $i < d$ and recursively define $a_{n + d} = - (c_{1} a_{n + d - 1} + \dots + c_{d} a_{n})$ ; this produces exactly one recurrence sequence with those initial values.

1.2L1L3

For a recurrence sequence with $F = \sum_{n \geq 0} a_{n} x^{n}$ , [L3] gives $[x^{m}] (Q F) = a_{m} + c_{1} a_{m - 1} + \dots + c_{d} a_{m - d}$ for $m \geq d$ , so every such coefficient is zero by [L1] and $P : = Q F$ has degree below $d$ or is zero.

1.3L2

Because $Q (0) = 1$ , division by $Q$ is defined formally, and $P \mapsto P / Q$ is a linear bijection from the numerator space to the proper fixed-denominator series space.

2.1step 1.1algebra

Initial-value extraction is linear, and step 1.1 is its linear inverse; hence the initial-value and recurrence-sequence spaces are linearly isomorphic.

2.2step 1.2L3

Conversely, if $P = Q F$ has no nonzero coefficient in degrees $m \geq d$ , the same coefficient identity read backwards gives the recurrence for every $n = m - d \geq 0$ ; thus $F \mapsto Q F$ is a linear bijection from the recurrence-sequence space to the degree- $< d$ numerator space.

3.1step 2.1step 2.2step 1.3L4∎

Coefficient extraction identifies the numerator space with $K^{d}$ , and [L4] gives its dimension $d$ ; the linear isomorphisms in steps 2.1, 2.2 and 1.3 therefore give dimension $d$ for all four spaces.

Depends on

Used by

Dependency tree · two levels

26 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)
M. Waldschmidt, Linear Recurrence Sequences VI, slides 5-18 (standard reference, not scraped)

The initial-value, recurrence-sequence, numerator and fixed-denominator rational-series spaces all have dimension dd