Exact realization of finite-history polynomials by bounded contracting SAS

Proved

ReservoirSAS.polynomial_sas_realization

by con · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebrapolynomialreservoir-computingstate-affine-system

Fix a real number $0<\kappa<1$ and a real polynomial $f$ in finitely many history coordinates $z_0,z_1,\ldots$ . There exist a finite state dimension, a matrix polynomial $p$ , a vector polynomial $q$ , and a linear readout vector $W$ , such that

\|p(u)v\|\le\kappa\|v\|,\qquad \|q(u)\|\le\kappa\quad (u\in[-1,1]),

and, for every bounded input history $z_k\in[-1,1]$ , there is a state trajectory satisfying

x_k=p(z_k)x_{k+1}+q(z_k),\qquad \|x_k\|\le\frac\kappa{1-\kappa},\qquad \langle W,x_0\rangle=f(z_0,z_1,\ldots).

The same coefficients and readout work for every input. There is no bound on $W$ . Existence of the bounded trajectory is explicitly part of the conclusion. The theorem concerns exact realization of finite polynomials, not approximation of arbitrary fading-memory targets.

This is a concrete realization subproblem for the source's nilpotent SAS mechanism. It is separated here from polynomial density so that the open construction can be developed independently. Mathlib's multivariate polynomials over $\mathbb N$ have finite support, so the statement requires only finite-dimensional systems.

Preamble

import Definitions.Def_ReservoirESN
import Definitions.Def_ReservoirSAS
import Mathlib.Algebra.MvPolynomial.Eval

open ReservoirESN ReservoirSAS

Formal statement

namespace ReservoirSAS
theorem polynomial_sas_realization (κ : ℝ) (hκ0 : 0 < κ) (hκ1 : κ < 1)
    (f : MvPolynomial ℕ ℝ) :
    ∃ (N r s : ℕ) (P : Fin r → Matrix (Fin N) (Fin N) ℝ)
      (Q : Fin s → EuclideanSpace ℝ (Fin N)) (W : EuclideanSpace ℝ (Fin N)),
      MatPolyOpBound P κ ∧ VecPolyBound Q κ ∧
      ∀ z : ℕ → ℝ, (∀ k, z k ∈ Set.Icc (-1 : ℝ) 1) →
        ∃ x : ℕ → EuclideanSpace ℝ (Fin N),
          (∀ k, ‖x k‖ ≤ κ / (1 - κ)) ∧ IsSASSolution P Q z x ∧
          inner ℝ W (x 0) = MvPolynomial.eval z f := by sorry
end ReservoirSAS

Source

L. Grigoryeva and J.-P. Ortega, Universal discrete-time reservoir computers with stochastic inputs and linear readouts using non-homogeneous state-affine systems, JMLR 19(24) (2018), https://jmlr.org/papers/volume19/18-020/18-020.pdf. Remark 12, p. 10 (finite-memory nilpotent linear systems); Proposition 17 and equations (3.21)–(3.23), p. 12 (polynomial algebra mechanism); Theorem 19 and Appendix 6.10, pp. 13 and 30–31 (nilpotent SAS universality). This exact finite-polynomial realization is a derived construction isolated here, not a verbatim source theorem. A concrete route uses one scaled shift chain for each monomial, then a block direct sum and compensating linear readout; choosing the scale sufficiently small enforces the Euclidean operator and vector bounds.

View graph