Exact contracting SAS realization of one history monomial

Proved

ReservoirSAS.monomial_sas_realization

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

linear-algebramonomialsreservoir-computingstate-affine-system

Let $0<\kappa<1$ and let $d:\mathbb N\to\mathbb N$ have finite support. There exists a finite-dimensional state-affine system with polynomial state-transition and forcing maps satisfying

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

and a linear readout $W$ such that, for every input history $z_k\in[-1,1]$ , there exists a trajectory with

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=\prod_{j\in\operatorname{supp}(d)}z_j^{d_j}.

All system coefficients and the readout are chosen independently of the input. The empty support is included, with product equal to one, so constants are covered. The readout is unrestricted in size.

This isolates the single-monomial construction in finite-history polynomial realization. Scalar polynomial coefficients can subsequently be placed in the readout without changing the dynamics or their bounds. The statement is a derived finite-chain construction for the source's nilpotent SAS framework, not a verbatim separately numbered result.

Preamble

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

open ReservoirSAS

Formal statement

namespace ReservoirSAS
theorem monomial_sas_realization (κ : ℝ) (hκ0 : 0 < κ) (hκ1 : κ < 1)
    (d : ℕ →₀ ℕ) :
    ∃ (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) = d.prod (fun j e => z j ^ e) := 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. Appendix 6.5, p. 25, the upper-shift nilpotent construction; equations (3.11), (3.14), Proposition 17, and Theorem 19 / Appendix 6.10, pp. 10–13 and 30–31. This monomial construction is a concrete refinement: scaled superdiagonal entries depend polynomially on the current input, with a terminal monomial forcing term. Exact matrix coefficient encoding, Euclidean bounds, and the readout identity remain the proof obligation.

View graph