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

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.

givenL1construct

1.2

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.

L1L3

1.3

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

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

step 1.1algebra

2.2

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.

step 1.2L3

3.1

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.

step 2.1step 2.2step 1.3L4∎

Depends on

Used by

Dependency tree · next 3 levels

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