TheoremStatement: Literature-sourcedProof: 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.

The Hadamard product of two rational formal power series over a field is rational

Statement

Let $K$ be a field. If $F = \sum_{n \geq 0} a_{n} x^{n}$ and $G = \sum_{n \geq 0} b_{n} x^{n}$ are rational formal power series over $K$ , then their Hadamard product

$F * G : = \sum_{n \geq 0} a_{n} b_{n} x^{n}$

is rational.

Facts & Assumptions

Given: Rational series $F = \sum a_{n} x^{n}$ and $G = \sum b_{n} x^{n}$ over a field $K$ .

[L1]

A coefficient sequence has a rational generating function exactly when it is eventually linearly recurrent (A coefficient sequence is eventually linearly recurrent if and only if its formal generating function is rational).

[L2]

A linearly independent subset of a vector space spanned by $m$ vectors has at most $m$ elements (If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $N$ ).

Proof

technique · direct

1.1givenL1

By [L1], after deleting finite prefixes the sequences $a$ and $b$ satisfy recurrences of orders $d$ and $e$ . Hence all shifts of the first tail lie in the span of its first $d$ shifts, and all shifts of the second tail lie in the span of its first $e$ shifts.

2.1step 1.1L1

If $d = 0$ or $e = 0$ , one tail and hence the product tail is zero, so [L1] already proves rationality. It remains to take $d, e \geq 1$ .

3.1step 1.1step 2.1algebra

Let $W$ be the span, inside the vector space of $K$ -valued sequences, of the $d e$ coefficientwise products $(S^{i} a) (S^{j} b)$ with $0 \leq i < d$ and $0 \leq j < e$ . Every simultaneous shift $S^{k} (a_{n} b_{n}) = (S^{k} a) (S^{k} b)$ belongs to $W$ by bilinear expansion.

4.1step 3.1L2algebra

By [L2], among any $d e + 1$ simultaneous shifts of the product tail there is a nontrivial linear dependence. Remove initial and terminal zero coefficients from such a relation and normalise its last coefficient to $1$ ; the remaining first coefficient is nonzero and the relation is an eventual constant-coefficient recurrence for $(a_{n} b_{n})$ .

5.1step 1.1step 2.1step 4.1L1∎

Applying [L1] to the product sequence in step 4.1 proves that $F * G$ is rational in the positive-order case. Together with step 2.1, this covers all rational inputs, and finite prefixes discarded in step 1.1 do not affect eventual recurrence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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., Proposition 4.2.5 (standard reference, not scraped)