[proofplan]
Because $\check{P}(0) = 1$, $\check{P}$ is a unit in $\mathbb{F}_2[[X]]$, so the rational expression $G(X) = A(X)/\check{P}(X)$ is equivalent to the polynomial identity $G(X)\, \check{P}(X) = A(X)$. The strategy is to compute the coefficient of $X^n$ in the product $G(X)\, \check{P}(X)$ explicitly and identify this coefficient, for $n \geq d$, with the LFSR recurrence. The degree condition $\deg A < d$ is then equivalent to vanishing of all coefficients $[X^n]\bigl(G\, \check{P}\bigr) = 0$ for $n \geq d$, which is precisely the LFSR recurrence holding for all $n \geq d$.
[/proofplan]
[step:Write $\check{P}$ in a form suitable for coefficient extraction]
Expanding the definition,
\begin{align*}
\check{P}(X) = 1 - \sum_{i=0}^{d-1} a_i X^{d-i}.
\end{align*}
Reindex the sum using $j = d - i$, so $i = d - j$ and $j$ ranges from $1$ to $d$ as $i$ ranges from $d-1$ down to $0$:
\begin{align*}
\check{P}(X) = 1 - \sum_{j=1}^{d} a_{d-j} X^{j} = \sum_{j=0}^{d} b_j X^j, \quad \text{where } b_0 = 1,\ b_j = -a_{d-j} \text{ for } 1 \leq j \leq d.
\end{align*}
(Over $\mathbb{F}_2$, $-a_{d-j} = a_{d-j}$, but we keep the sign for conceptual clarity in the computation below.)
[/step]
[step:Compute the coefficient of $X^n$ in $G(X)\, \check{P}(X)$ for $n \geq d$]
The product of formal power series in $\mathbb{F}_2[[X]]$ is given by Cauchy convolution:
\begin{align*}
G(X)\, \check{P}(X) = \sum_{n=0}^{\infty} \left( \sum_{j=0}^{n} b_j y_{n-j} \right) X^n.
\end{align*}
For $n \geq d$, the outer sum terminates at $j = d$ because $b_j = 0$ for $j > d$:
\begin{align*}
[X^n] \bigl(G \cdot \check{P}\bigr) = \sum_{j=0}^{d} b_j y_{n-j} = b_0 y_n + \sum_{j=1}^{d} b_j y_{n-j} = y_n - \sum_{j=1}^{d} a_{d-j} y_{n-j}.
\end{align*}
Reindexing the remaining sum with $i = d - j$ (so $j = d - i$ ranges from $d$ to $1$ as $i$ ranges from $0$ to $d-1$, and $y_{n-j} = y_{n - d + i}$):
\begin{align*}
\sum_{j=1}^{d} a_{d-j} y_{n-j} = \sum_{i=0}^{d-1} a_i y_{n - d + i}.
\end{align*}
Substituting back,
\begin{align*}
[X^n] \bigl(G \cdot \check{P}\bigr) = y_n - \sum_{i=0}^{d-1} a_i y_{n - d + i} \qquad \text{for every } n \geq d. \qquad (\ast)
\end{align*}
[guided]
The product of two formal power series is given by the Cauchy convolution rule: the coefficient of $X^n$ in the product is $\sum_{j=0}^{n} (\text{coef of } X^j \text{ in first}) \cdot (\text{coef of } X^{n-j} \text{ in second})$.
For $G(X) \check{P}(X)$ this reads
\begin{align*}
[X^n] \bigl(G \cdot \check{P}\bigr) = \sum_{j=0}^{n} b_j y_{n - j},
\end{align*}
where $b_j$ is the coefficient of $X^j$ in $\check{P}$.
Here is the helpful observation: $\check{P}$ is a polynomial of degree $d$, so $b_j = 0$ for all $j > d$. Hence **for $n \geq d$** the convolution sum truncates to $\sum_{j=0}^{d} b_j y_{n-j}$ (it does not matter that $n$ is larger — the terms $j > d$ vanish). This is what allows us to link the product coefficient to the LFSR recurrence.
Substituting $b_0 = 1$ and $b_j = -a_{d-j}$ for $1 \leq j \leq d$, and reindexing via $i = d - j$:
\begin{align*}
[X^n] \bigl(G \cdot \check{P}\bigr) = y_n - \sum_{i=0}^{d-1} a_i y_{n - d + i}.
\end{align*}
This is precisely the "defect" of the LFSR recurrence at time $n$: it is zero exactly when the recurrence $y_n = \sum_{i=0}^{d-1} a_i y_{n-d+i}$ holds, and nonzero when it fails. Why the sign flip between the polynomial $P(X) = X^d - \sum a_i X^i$ and the coefficients of $\check{P}$? Reversal swaps "leading" and "trailing" coefficients, and the leading term $X^d$ of $P$ becomes the constant term $1$ of $\check{P}$, while the trailing terms $-a_i X^i$ become the higher-order terms $-a_i X^{d-i}$ of $\check{P}$. Bookkeeping takes care of the rest.
[/guided]
[/step]
[step:The LFSR recurrence is equivalent to $G(X)\, \check{P}(X)$ being a polynomial of degree less than $d$]
By $(\ast)$, the coefficient $[X^n]\bigl(G \cdot \check{P}\bigr)$ for $n \geq d$ is exactly the defect $y_n - \sum_{i=0}^{d-1} a_i y_{n-d+i}$ of the LFSR recurrence at index $n$. Therefore:
- $(y_n)_{n \geq 0}$ satisfies the LFSR recurrence for $P$ at every $n \geq d$
- $\iff y_n - \sum_{i=0}^{d-1} a_i y_{n - d + i} = 0$ for all $n \geq d$
- $\iff [X^n]\bigl(G \cdot \check{P}\bigr) = 0$ for all $n \geq d$
- $\iff G(X)\, \check{P}(X)$ is a polynomial of degree at most $d - 1$.
Let $A(X) := G(X)\, \check{P}(X)$. The equivalence says: the stream satisfies the recurrence if and only if $A(X) \in \mathbb{F}_2[X]$ with $\deg A < d$.
[/step]
[step:Convert between the polynomial identity and the rational form]
We verify that $\check{P}$ is a unit in $\mathbb{F}_2[[X]]$. A formal power series $\sum_{j \geq 0} b_j X^j$ is a unit in $\mathbb{F}_2[[X]]$ if and only if its constant term $b_0$ is a unit in $\mathbb{F}_2$, i.e., equals $1$. Here $\check{P}(0) = b_0 = 1$, so $\check{P}$ is a unit in $\mathbb{F}_2[[X]]$ and $\check{P}^{-1} \in \mathbb{F}_2[[X]]$ exists.
Therefore, within $\mathbb{F}_2[[X]]$, the identity
\begin{align*}
G(X)\, \check{P}(X) = A(X)
\end{align*}
is equivalent to
\begin{align*}
G(X) = \frac{A(X)}{\check{P}(X)}.
\end{align*}
Combining with Step 3:
- **($\Rightarrow$)** If $(y_n)$ satisfies the LFSR recurrence for $P$, then $G \cdot \check{P}$ is a polynomial $A$ with $\deg A < d$, so $G = A/\check{P}$ with $\deg A < d = \deg \check{P}$.
- **($\Leftarrow$)** If $G = A/\check{P}$ with $A \in \mathbb{F}_2[X]$ and $\deg A < d$, then $G \cdot \check{P} = A$ as power series, so $[X^n]\bigl(G \cdot \check{P}\bigr) = 0$ for $n \geq d$, so by $(\ast)$ the LFSR recurrence for $P$ holds at every $n \geq d$.
This establishes the equivalence and completes the proof.
[guided]
To close the argument we need two separate facts, which we assemble here.
**First**, $\check{P}$ is invertible in $\mathbb{F}_2[[X]]$. This is a standard fact about formal power series: $f = \sum b_j X^j \in R[[X]]$ is a unit if and only if its constant term $b_0$ is a unit in $R$. For us, $R = \mathbb{F}_2$, and the only unit is $1$. We verify: $\check{P}(0) = X^d P(1/X) \big|_{X=0}$ — but plugging $X = 0$ into $X^d P(1/X)$ requires care because $P(1/X)$ blows up. Instead, read off the constant term of $\check{P}$ directly from the expansion $\check{P}(X) = 1 - \sum_{i=0}^{d-1} a_i X^{d-i}$: every term in the sum has $X^{d-i}$ with $d - i \geq 1$, so the constant term is $1$. Hence $\check{P}$ is a unit in $\mathbb{F}_2[[X]]$.
This means the polynomial identity
\begin{align*}
G(X) \cdot \check{P}(X) = A(X)
\end{align*}
is rigorously equivalent to the fraction identity $G(X) = A(X)/\check{P}(X)$ in $\mathbb{F}_2[[X]]$.
**Second**, we assemble both directions of the if-and-only-if.
Forward direction: assume $(y_n)$ satisfies the LFSR recurrence. By Step 3, $G \cdot \check{P}$ is a polynomial $A$ with $\deg A < d$. Dividing by $\check{P}$ gives $G = A/\check{P}$ with the required degree bound.
Reverse direction: assume $G = A/\check{P}$ with $A \in \mathbb{F}_2[X]$ and $\deg A < d$. Multiplying by $\check{P}$ (allowed because $\check{P}$ is a unit in $\mathbb{F}_2[[X]]$), $G \cdot \check{P} = A$ as a formal power series. The right-hand side has only finitely many nonzero coefficients, all at indices strictly less than $d$. Hence $[X^n](G \cdot \check{P}) = 0$ for all $n \geq d$. By the identity $(\ast)$ from Step 2, this means the LFSR recurrence holds at every $n \geq d$.
The two directions together give the biconditional. Note what we have *not* claimed: we do not assert that $A$ is unique, but it is: if $G \cdot \check{P} = A_1 = A_2$ in $\mathbb{F}_2[[X]]$, then $A_1 = A_2$ in $\mathbb{F}_2[X]$ because the embedding $\mathbb{F}_2[X] \hookrightarrow \mathbb{F}_2[[X]]$ is injective. The initial conditions $y_0, y_1, \ldots, y_{d-1}$ determine $A$ through the first $d$ convolution coefficients.
[/guided]
[/step]
