Finite superposition of SAS realizations with a shared norm budget

Proved

ReservoirSAS.sas_finite_sum_realization

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

direct-sumlinear-algebrareservoir-computingstate-affine-system

Let $S$ be a finite set of indices, let $F_i$ be real-valued functionals on scalar histories, and fix $0<\kappa<1$ . Put $m=|S|$ and $\delta=\kappa/(m+1)$ . Assume that for each $i\in S$ there is a polynomial state-affine system and a linear readout realizing $F_i$ exactly on every history in $[-1,1]^{\mathbb N}$ , with transition-operator and forcing-vector bounds $\delta$ , and with a realizing trajectory bounded by $\delta/(1-\delta)$ .

Then one finite-dimensional polynomial state-affine system with transition-operator and forcing-vector bounds $\kappa$ realizes their sum:

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=\sum_{i\in S}F_i(z).

A bounded realizing trajectory must exist for every admissible input. State dimensions, coefficient counts, and readout sizes of the components may differ. The empty set is included and yields the zero functional.

This is a quantitative finite-family form of the source's direct-sum closure result. The reduced component budget is explicit because concatenating forcing vectors can increase their Euclidean norm. No continuity or fading-memory hypothesis on the named functionals is added: their exact SAS realizations are the hypotheses.

Preamble

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

open ReservoirSAS

Formal statement

namespace ReservoirSAS
theorem sas_finite_sum_realization {ι : Type*} (S : Finset ι)
    (F : ι → (ℕ → ℝ) → ℝ) (κ : ℝ) (hκ0 : 0 < κ) (hκ1 : κ < 1)
    (hcomponents : ∀ i ∈ S,
      ∃ (N r s : ℕ) (P : Fin r → Matrix (Fin N) (Fin N) ℝ)
        (Q : Fin s → EuclideanSpace ℝ (Fin N)) (W : EuclideanSpace ℝ (Fin N)),
        MatPolyOpBound P (κ / (S.card + 1)) ∧ VecPolyBound Q (κ / (S.card + 1)) ∧
        ∀ z : ℕ → ℝ, (∀ k, z k ∈ Set.Icc (-1 : ℝ) 1) →
          ∃ x : ℕ → EuclideanSpace ℝ (Fin N),
            (∀ k, ‖x k‖ ≤ (κ / (S.card + 1)) / (1 - κ / (S.card + 1))) ∧
            IsSASSolution P Q z x ∧ inner ℝ W (x 0) = F i z) :
    ∃ (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) = ∑ i ∈ S, F i z := 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. Proposition 17(i), equation (3.21), p. 12; coefficient padding in equation (3.19), p. 11; Lemma 38(i), pp. 29–30. This is a derived finite-family version with additional explicit forcing and state bounds. Direct sums use delta=kappa/(card(S)+1), allowing the estimates ||q||≤card(S)*delta≤kappa and ||x_k||≤card(S)*delta/(1-delta)≤kappa/(1-kappa).

View graph