The product of two state-affine systems is state-affine: its matrix is polynomial

Proved

PolyAssembly.prodMat_eval

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

kronecker-productmachine-learningreservoir-computingstate-affine-system

Let two state-affine systems be given by coefficient families, so that their matrices and affine terms are polynomial in the input:

p_i(z) = \sum_m z^m P^i_m, \qquad q_i(z) = \sum_m z^m Q^i_m .

The theorem asserts that the matrix of the product system — the block-triangular matrix acting on the augmented state $(x_1, x_2, x_1\otimes x_2)$ — is itself the evaluation of a single coefficient family:

\sum_{i} z^{\deg i}\, C_i \;=\; \mathrm{prodMat}\bigl(p_1(z),\, q_1(z),\, p_2(z),\, q_2(z)\bigr) .

The degrees convolve: they are simple for the two diagonal blocks, and sums $m+n$ for the cross blocks and the tensor block.

What this completes. Together with the trajectory-level identity — the augmented state solves the product recursion and the readout returns the product of the two outputs — this establishes that the product of two state-affine systems is a state-affine system. That is the closure under products of Proposition 3.10, and hence the algebra property of the family of state-affine reservoir functionals, which is one of the two hypotheses of the Stone-Weierstrass argument behind their universality; the other is that the family separates points.

Formalization Note The coefficients are indexed by a disjoint union with one degree function per family of blocks, rather than uniformly over pairs of degrees. The alternative would force the diagonal blocks to be written with a test on whether the second index vanishes, which is harder to manipulate and introduces a degenerate case when there are no coefficients at all. The statement holds for every real $z$ , including zero, where the convention $0^0 = 1$ makes the constant terms contribute. No positivity or bound on the coefficients is assumed: this is an identity of matrices, not an estimate.

Preamble

import Mathlib
import Definitions.Def_SASAlgebra
import Definitions.Def_PolyAssembly

open Matrix SASAlgebra PolyAssembly

Formal statement

namespace PolyAssembly

variable {N₁ N₂ r : ℕ}

theorem prodMat_eval (P₁ : Fin r → Matrix (Fin N₁) (Fin N₁) ℝ)
    (Q₁ : Fin r → (Fin N₁ → ℝ)) (P₂ : Fin r → Matrix (Fin N₂) (Fin N₂) ℝ)
    (Q₂ : Fin r → (Fin N₂ → ℝ)) (z : ℝ) :
    ∑ i : ProdIdx r, (z ^ prodDeg i) • prodCoef P₁ Q₁ P₂ Q₂ i
      = prodMat (polyEval P₁ z) (vpolyEval Q₁ z)
                (polyEval P₂ z) (vpolyEval Q₂ z) := by sorry

end PolyAssembly

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, Proposition 3.10 and equations (3.19)-(3.22); the coefficient half of part (ii), completing the trajectory-level identity.

View graph