25. The finite learned-realization theorem
On this page · Permalink · Source line 1095
The preceding results combine into a concrete completion of one part of the learning problem. This is the integrated identification claim for the autonomous linear sector.
Proposition 25: Observationally grounded finite linear realization
Assume all of the following:
The data come from an autonomous finite-dimensional linear process with declared outputs \(y_t=Cx_t\).
A delay length \(h\) satisfies \(\operatorname{rank}O_{h+1}=\operatorname{rank}O_h\).
Exact observed input windows in \(Z_-\) span \(V_h=\operatorname{im}O_h\), and \(Z_+\) records their true one-step successor windows.
Then an algorithm using only \((Z_-,Z_+)\) recovers the unique transition on \(V_h\). Initialized with a fully observed length-\(h\) window, it predicts every later output exactly. Any lossless atlas of \(V_h\), any complete packet decomposition of that space, and every coherently transported realization of the learned transition preserve the same predictions. Hidden variables outside the observable quotient need not be recovered.
If the fixed-space assumptions of Proposition 16 replace exact observations, that proposition bounds operator error. Whenever the resulting transition defects and Lipschitz constants satisfy Proposition 18, its product-sum bound controls the output prediction error. A common contraction margin yields the stated uniform bound.
Read proof · Recorded Lean scope · Permalink · Source line 1099
Proof
Proposition 14 gives the unique true transition \(D_h\) on \(V_h\). Because the observed windows span \(V_h\), Proposition 15 identifies exactly its restriction, which is the entire required operator. Equality of the learned and true states follows by induction after initialization. The current output is the last block of the history state. Propositions 1–4 preserve state reconstruction, transport and complete decomposition, so they preserve that output sequence. The perturbation statement is the direct composition of Propositions 16 and 18 with the declared output decoder. \(\square\)
This establishes an actual route from observations to a composable algebraic signal model under explicit finite assumptions. It is more than a fit on a few points. It is also less than unrestricted nonlinear world-model discovery. In particular, the algorithm does not infer assumptions 1–3 merely by returning a matrix. The accompanying certificate keeps the data-verified identities separate from those model assumptions.