Echo state property of a contracting state-affine system (Prop. 3.7)

Proved

ReservoirSAS.sas_esp_of_contracting_polynomial

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

fixed-pointmachine-learningreservoir-computingstate-affine-system

Consider a non-homogeneous state-affine system $x_k = p(z_k)x_{k+1} + q(z_k)$ driven by an input sequence with values in $[-1,1]$ . Suppose $K_1 < 1$ bounds the operator norm of $p(z)$ and $K_2 > 0$ bounds the norm of $q(z)$ , both uniformly over $z \in [-1,1]$ . Then there is exactly one state sequence bounded by $K_2/(1-K_1)$ satisfying the system equation.

This is Proposition 3.7 of the source: contractivity of the state map gives the echo state property, and the explicit ceiling $K_2/(1-K_1)$ on the states. The echo state property is what makes the map from input history to state well defined, and hence what makes the SAS functional — the object the universality theorem approximates with — exist at all.

The system is a contracting reservoir map: the state map contracts with ratio $K_1$ uniformly in the input, and the ball of radius $K_2/(1-K_1)$ is invariant, since $K_1 \cdot K_2/(1-K_1) + K_2 = K_2/(1-K_1)$ . The statement therefore specializes a result already published on this platform rather than requiring a new mechanism.

Formalization Note Uniqueness is asserted within the class of sequences bounded by $K_2/(1-K_1)$ ; nothing is claimed about unbounded solutions. The recursion determines $x_k$ from $x_{k+1}$ , so it constrains the whole sequence and admits no initial condition. The hypothesis $K_2 > 0$ makes the invariant ball nondegenerate.

Preamble

import Mathlib
import Definitions.Def_ReservoirESN
import Definitions.Def_ReservoirSAS

open Matrix Metric ReservoirESN ReservoirSAS

Formal statement

namespace ReservoirSAS

theorem sas_esp_of_contracting_polynomial {N r s : ℕ}
    (P : Fin r → Matrix (Fin N) (Fin N) ℝ) (Q : Fin s → EuclideanSpace ℝ (Fin N))
    (K₁ K₂ : ℝ) (hK₁0 : 0 ≤ K₁) (hK₁ : K₁ < 1) (hK₂ : 0 < K₂)
    (hP : MatPolyOpBound P K₁) (hQ : VecPolyBound Q K₂)
    (z : ℕ → ℝ) (hz : ∀ k, z k ∈ Set.Icc (-1 : ℝ) 1) :
    ∃! x : ℕ → EuclideanSpace ℝ (Fin N),
      (∀ k, ‖x k‖ ≤ K₂ / (1 - K₁)) ∧ IsSASSolution P Q z x := 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. 10, Proposition 3.7: under max_z ||p(z)||_2 < 1 the system has the echo state property, with the state bound ||x_t|| <= K_2/(1-K_1) of eq. (3.16).

Read-back

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

Read-back — `sas_esp_of_contracting_polynomial`

Data and binders. Three natural numbers $N$ , $r$ , $s$ are fixed; they are implicit and completely arbitrary, so each of them may be $0$ . One is given:

a finite family of real $N \times N$ matrices $P_0, \dots, P_{r-1}$ , written as a map $P : \{0,\dots,r-1\} \to \mathbb{R}^{N\times N}$ ;
a finite family of vectors $Q_0, \dots, Q_{s-1}$ in $\mathbb{R}^N$ , the space carrying its Euclidean ( $\ell^2$ ) norm; every norm $\lVert\cdot\rVert$ below is that Euclidean norm;
two real numbers $K_1, K_2$ ;
a real sequence $z : \mathbb{N} \to \mathbb{R}$ (scalar-valued, not vector-valued).

These families define, for a real argument $t$ , the matrix-valued and vector-valued polynomials

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

Empty sums are $0$ : if $r = 0$ then $p \equiv 0$ , and if $s = 0$ then $q \equiv 0$ . The convention $t^0 = 1$ holds also at $t = 0$ , so $p(0) = P_0$ and $q(0) = Q_0$ when $r, s \ge 1$ .

Hypotheses. All of the following are assumed:

$0 \le K_1$ ;
$K_1 < 1$ ;
$0 < K_2$ ;
(uniform operator bound on $p$ ) for every $t \in [-1,1]$ and every vector $v \in \mathbb{R}^N$ , $\lVert p(t)\,v \rVert \le K_1 \lVert v \rVert$ — i.e. the spectral norm of $p(t)$ is at most $K_1$ for all $t$ in the closed interval $[-1,1]$ ;
(uniform bound on $q$ ) for every $t \in [-1,1]$ , $\lVert q(t) \rVert \le K_2$ ;
every term of the input sequence lies in the closed interval: $z_k \in [-1,1]$ for all $k \in \mathbb{N}$ .

Note that (1)–(3) are stated separately from (4)–(5); nothing forces $K_1$ or $K_2$ to be the least such constants. Since $K_1 < 1$ , the quantity $1 - K_1$ is strictly positive, so the ratio $K_2/(1-K_1)$ below is an ordinary positive real with no division-by-zero convention involved.

Conclusion. There exists exactly one sequence of vectors $x : \mathbb{N} \to \mathbb{R}^N$ , i.e. one function $k \mapsto x_k$ , satisfying both of the following:

\text{(a)}\quad \lVert x_k \rVert \;\le\; \frac{K_2}{1-K_1} \quad \text{for every } k \in \mathbb{N},

\text{(b)}\quad x_k \;=\; p(z_k)\, x_{k+1} \;+\; q(z_k) \quad \text{for every } k \in \mathbb{N}.

Uniqueness is uniqueness of the pair of properties taken together: any other sequence $y$ that both is bounded by $K_2/(1-K_1)$ at every index and satisfies the same recursion is equal to $x$ as a function on all of $\mathbb{N}$ . The statement asserts nothing about sequences satisfying (b) alone, nor about sequences obeying (b) with some larger uniform bound.

The recursion (b) runs "backwards" in the index: $x_k$ is expressed in terms of $x_{k+1}$ , so each term is determined by its successor rather than its predecessor, and there is no initial condition at $k=0$ and no terminal index.

Degenerate cases included. $N = 0$ is allowed, in which case $\mathbb{R}^N$ is the zero space and the claim is trivially about the single zero sequence. $r = 0$ makes $p \equiv 0$ , so hypothesis (4) holds for any $K_1 \ge 0$ and (b) reduces to $x_k = q(z_k)$ . $s = 0$ makes $q \equiv 0$ , so (5) holds for any $K_2 > 0$ and the unique sequence is identically zero. The hypotheses are jointly satisfiable (take $P \equiv 0$ ), so the statement is not vacuous.

The proof is not supplied: the declaration's body is sorry.

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

Echo state property of a contracting state-affine system (Prop. 3.7)

Read-back — sas_esp_of_contracting_polynomial

Read-back — `sas_esp_of_contracting_polynomial`