Universality of SAS reservoir computers (Thm. 3.12)

Proved

ReservoirSAS.sas_universal

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

machine-learningreservoir-computingstate-affine-systemuniversal-approximation

Let $H$ be a functional on scalar input sequences bounded by one, with the fading memory property. The theorem asserts that for every $\varepsilon \in (0,1)$ there exist polynomials $p$ , $q$ and a readout vector $W$ , with both polynomial bounds below $1-\varepsilon$ , such that the associated state-affine system approximates $H$ uniformly:

\sup_z \bigl| H(z) - W^{\top} x_0(z) \bigr| < \varepsilon .

This is Theorem 3.12 of the source. It is the density result of reservoir computing: the family of state-affine systems with linear readouts is dense in the fading memory category. Every later universality theorem for reservoir families rests on it, including the one for echo state networks, whose proof replaces the target filter by a state-affine system before replacing it by a network.

The proof is not constructive in the naive sense: the target is an arbitrary fading memory filter given by no formula. It proceeds by showing that the SAS functionals form a polynomial algebra separating points and containing the constants, then applying a Stone-Weierstrass argument on a space of inputs made compact by the weighted topology.

Formalization Note A single $\varepsilon$ controls both the approximation accuracy and the polynomial bounds $1-\varepsilon$ , exactly as in the source; it is not an independent tolerance. The state ceiling $(1-\varepsilon)/\varepsilon$ appearing in the conclusion is what the supporting target delivers for those bounds, and it is that target which guarantees such a state sequence exists and is unique, so the approximation clause is not vacuous. The conclusion is stated for every bounded solution rather than for a distinguished one, which is stronger. Inputs are scalar, as in Section 3 of the source. The fading memory property of the target is the one already published on the platform, stated for a functional rather than a filter; the two are in linear bijection.

Preamble

import Mathlib
import Definitions.Def_ReservoirESN
import Definitions.Def_ReservoirSAS

open Matrix Metric ReservoirESN ReservoirSAS

Formal statement

namespace ReservoirSAS

theorem sas_universal
    (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1) (w : ℕ → ℝ) (hw : IsWeighting w)
    (H : (ℕ → ℝ) → ℝ) (hH : FunctionalFMP H 1 w) :
    ∃ (N r s : ℕ) (P : Fin r → Matrix (Fin N) (Fin N) ℝ)
      (Q : Fin s → EuclideanSpace ℝ (Fin N)) (W : EuclideanSpace ℝ (Fin N)),
      MatPolyOpBound P (1 - ε) ∧ VecPolyBound Q (1 - ε) ∧
      ∀ z : ℕ → ℝ, (∀ k, z k ∈ Set.Icc (-1 : ℝ) 1) →
        ∀ x : ℕ → EuclideanSpace ℝ (Fin N), IsSASSolution P Q z x →
          (∀ k, ‖x k‖ ≤ (1 - ε) / ε) →
          |H z - inner ℝ W (x 0)| < ε := by sorry

end ReservoirSAS

Source

L. Grigoryeva, J.-P. Ortega, Universal discrete-time reservoir computers with stochastic inputs and linear readouts using non-homogeneous state-affine systems, Journal of Machine Learning Research 19(24) (2018), 1-40, https://arxiv.org/abs/1712.00754, p. 12, Theorem 3.12: the family of SAS functionals with M_p, M_q < 1 - epsilon is dense in the fading memory category; any such filter is uniformly approximated within epsilon.

Read-back

What the Lean code literally says, in plain math · claude-opus-5

The statement fixes a real number $\varepsilon$ subject to $0 < \varepsilon$ and $\varepsilon < 1$ ; a sequence $w : \mathbb{N} \to \mathbb{R}$ assumed to be a weighting sequence, meaning $w_k > 0$ and $w_k \le 1$ for every $k$ , $w$ is non-increasing, and $w_k \to 0$ as $k \to \infty$ ; and a functional $H$ sending a real-valued sequence $z : \mathbb{N} \to \mathbb{R}$ to a real number $H(z)$ . The functional is assumed to have the fading-memory property at input level $1$ relative to $w$ , which unfolds to:

\forall \eta > 0,\ \exists \delta > 0,\ \forall z, z' : \mathbb{N} \to \mathbb{R},\quad \Big(\forall k,\ |z_k| \le 1\Big) \wedge \Big(\forall k,\ |z'_k| \le 1\Big) \wedge \Big(\forall k,\ |z_k - z'_k|\, w_k \le \delta\Big) \ \Longrightarrow\ |H(z) - H(z')| < \eta .

This says nothing about $H$ on sequences that leave $[-1,1]$ , and imposes no bound on the values of $H$ .

Under these hypotheses the theorem asserts the existence of three natural numbers $N, r, s$ , a family of $r$ real $N \times N$ matrices $P_0, \dots, P_{r-1}$ , a family of $s$ vectors $Q_0, \dots, Q_{s-1}$ in the Euclidean space $\mathbb{R}^N$ , and one further vector $W \in \mathbb{R}^N$ , such that three conditions hold simultaneously. Write

p(z) := \sum_{j=0}^{r-1} z^{j} P_j \in \mathbb{R}^{N \times N}, \qquad q(z) := \sum_{j=0}^{s-1} z^{j} Q_j \in \mathbb{R}^{N},

with $\|\cdot\|$ the Euclidean norm throughout.

(i) Matrix-polynomial bound. For every real $z \in [-1,1]$ and every vector $v \in \mathbb{R}^N$ , $\ \|p(z)\,v\| \le (1-\varepsilon)\,\|v\|$ . (This is stated vector-by-vector, not as a named operator norm.)

(ii) Vector-polynomial bound. For every real $z \in [-1,1]$ , $\ \|q(z)\| \le 1-\varepsilon$ .

(iii) Approximation clause. For every sequence $z : \mathbb{N} \to \mathbb{R}$ whose every term lies in $[-1,1]$ , and for every sequence of states $x : \mathbb{N} \to \mathbb{R}^N$ satisfying both

x_k = p(z_k)\, x_{k+1} + q(z_k) \quad \text{for every } k \in \mathbb{N}, \qquad\text{and}\qquad \|x_k\| \le \frac{1-\varepsilon}{\varepsilon} \quad \text{for every } k \in \mathbb{N},

one has the strict inequality

\Big| H(z) - \langle W, x_0\rangle \Big| < \varepsilon, \qquad \langle W, x_0\rangle = \sum_{i=0}^{N-1} W_i\, (x_0)_i .

Several features of the quantification deserve to be made explicit. The index $k$ runs over $\mathbb{N}$ and the recursion determines $x_k$ from the higher-indexed $x_{k+1}$ ; the term evaluated against $W$ is $x_0$ . The witnesses $N, r, s, P, Q, W$ are chosen before $z$ and $x$ , so a single system and a single readout vector must work for all admissible inputs; conversely they are chosen after $\varepsilon$ , $w$ and $H$ , so they may depend on all three. The sequence $w$ appears nowhere in the conclusion — it enters only through the hypothesis on $H$ . No bound whatsoever is placed on $\|W\|$ , and no relation is required between $N$ , $r$ and $s$ .

The numbers $N$ , $r$ , $s$ are unrestricted naturals and may be $0$ . With $r = 0$ the sum defining $p(z)$ is empty, so $p(z)$ is the zero matrix; with $s = 0$ , $q(z)$ is the zero vector; with $N = 0$ the space $\mathbb{R}^N$ is trivial, every state is $0$ and the inner product is $0$ . In each of those cases conditions (i) and (ii) hold automatically, since $1 - \varepsilon > 0$ .

The final clause asserts nothing about existence: it does not claim that an admissible input $z$ admits any state sequence satisfying the recursion, nor that a solution of the recursion satisfies the norm bound $\|x_k\| \le (1-\varepsilon)/\varepsilon$ . For any $z$ admitting no such bounded solution, the inequality holds vacuously. In the other direction the clause quantifies over all bounded solutions attached to a given $z$ , so whenever several exist, each of their readouts $\langle W, x_0\rangle$ must lie strictly within $\varepsilon$ of $H(z)$ .

Finally, the single parameter $\varepsilon$ plays three distinct roles that are tied together: the contraction factor $1-\varepsilon$ in (i), the vector bound $1-\varepsilon$ in (ii) and the state-norm ceiling $(1-\varepsilon)/\varepsilon$ in (iii), and the approximation accuracy $\varepsilon$ itself. Since $0 < \varepsilon < 1$ , we have $1-\varepsilon \in (0,1)$ and $(1-\varepsilon)/\varepsilon > 0$ . The accuracy claimed is exactly $\varepsilon$ , strictly, and not an arbitrary independent tolerance. The declaration carries no proof; its body is left unproved.

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by olivier · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph