6. Constructing the smallest closed linear refinement
On this page · Permalink · Source line 237
There is a constructive finite solution when the dynamics are a known finite family of linear maps \(L_u\) on a \(d\)-dimensional space. It identifies which additional observables are required, rather than merely requesting a larger state vector.
Let the initial summary be \(C_0x\). Regard its rows as linear observables. Starting from \(W_0=\operatorname{row}(C_0)\), define
Proposition 8: Minimal linear predictive completion
The sequence stabilizes after at most \(d-\dim W_0\) strict enlargements. Its limit \(W_*\) is the smallest row space containing \(W_0\) and invariant under right multiplication by every \(L_u\). If \(R\) is any full-row-rank matrix whose rows form a basis of \(W_*\), then
for suitable matrices \(H\) and \(B_u\). Therefore \(z=Rx\) retains the original summary and has exact reduced dynamics \(z_{t+1}=B_uz_t\). Every linear summary with those two properties has row space containing \(W_*\).
Read proof · Recorded Lean scope · Visual guide: Refinement closes an observable space · Permalink · Source line 248
Proof
The spaces are nested and have dimension at most \(d\). Equality at one step means invariance under every \(L_u\), so it is a fixed point. Containment in any invariant row space containing \(W_0\) follows by induction. The matrix identities express inclusion of the relevant rows in the basis \(R\). Conversely, if \(C_0=HR\) and \(RL_u=B_uR\), the row space of \(R\) is invariant and contains \(W_0\), so it contains every \(W_n\). \(\square\)
For one transition matrix this reduces to the span of the rows of
Its annihilator is the largest \(L\)-invariant subspace inside \(\ker C_0\), the standard unobservable-subspace construction [R2]. With several actions, observables pulled back through action words are required, but the linear span still stabilizes in finite dimension.
This gives a precise role for obstruction-driven refinement: add observable directions created by the dynamics until the chosen prediction variables close. It does not guarantee that the completion is small. In some systems \(W_*=X^*\) and exact memoryless closure needs the full state.
The theorem assumes the operators and relevant state are available. Applying it to estimated operators constructs closure for those estimates. It is not a proof that the real system has the same closure. If only \(C_0x\) is measured and the full \(x\) is unavailable, the augmented state \(Rx\) is not automatically accessible.