The tensor-augmented state of a product of affine recursions, and its readout

Proved

SASAlgebra.prod_isSolution

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

kronecker-productmachine-learningreservoir-computingstate-affine-system

Let two affine recursions be driven by the same scalar input sequence,

x_1(k) = p_1(z_k)\,x_1(k+1) + q_1(z_k), \qquad x_2(k) = p_2(z_k)\,x_2(k+1) + q_2(z_k),

with arbitrary matrix- and vector-valued coefficient maps. Then the augmented state $\bigl(x_1, x_2, x_1\otimes x_2\bigr)$ obeys an affine recursion of its own, with the block-triangular matrix

\begin{pmatrix} p_1 & 0 & 0 \\ 0 & p_2 & 0 \\ p_1\otimes q_2 & q_1\otimes p_2 & p_1\otimes p_2 \end{pmatrix}, \qquad \text{constant term } \bigl(q_1,\ q_2,\ q_1\otimes q_2\bigr),

and the readout $0 \oplus 0 \oplus (W_1 \otimes W_2)$ applied to it returns, at every instant, the product $\left(W_1\cdot x_1\right)\left(W_2\cdot x_2\right)$ of the two outputs.

This is the algebraic core of Proposition 3.10 of the source, the closure of state-affine reservoir functionals under products. What the identity exhibits is why the augmentation is unavoidable: the two cross terms act on $x_1$ and $x_2$ separately, so neither can be recovered from the tensor component alone, and the term $q_1 \otimes q_2$ is constant, so no homogeneous system produces it. That last point is exactly why the closure fails for linear reservoirs.

What this statement does and does not establish. It establishes the trajectory-level identity: the augmented state solves the displayed recursion, and the readout returns the product. It does not establish that the product system is itself a state-affine system in the sense of the definition — that would require showing the map $z \mapsto$ (product matrix) to be polynomial in $z$ , obtained by convolving the coefficient families. Each block is a product of polynomials, so this holds, but the assembly is not part of this statement. Anyone completing Proposition 3.10 will need that step on top of this one.

Formalization Note The coefficient maps are arbitrary functions of the input, with no polynomial structure assumed; the statement is correspondingly more general than the proposition it serves, and does not by itself carry the meaning "state-affine". The conclusion is a conjunction whose second half, the readout identity, is a pointwise algebraic fact using neither recursion hypothesis. The augmented state is indexed by a disjoint union, the block matrix being a rendering of that index type.

Preamble

import Mathlib
import Definitions.Def_SASAlgebra

open Matrix SASAlgebra

Formal statement

namespace SASAlgebra

theorem prod_isSolution {N₁ N₂ : ℕ}
    (p₁ : ℝ → Matrix (Fin N₁) (Fin N₁) ℝ) (q₁ : ℝ → (Fin N₁ → ℝ))
    (p₂ : ℝ → Matrix (Fin N₂) (Fin N₂) ℝ) (q₂ : ℝ → (Fin N₂ → ℝ))
    (W₁ : Fin N₁ → ℝ) (W₂ : Fin N₂ → ℝ)
    (z : ℕ → ℝ) (x₁ : ℕ → (Fin N₁ → ℝ)) (x₂ : ℕ → (Fin N₂ → ℝ))
    (h₁ : ∀ k, x₁ k = p₁ (z k) *ᵥ x₁ (k + 1) + q₁ (z k))
    (h₂ : ∀ k, x₂ k = p₂ (z k) *ᵥ x₂ (k + 1) + q₂ (z k)) :
    (∀ k, prodState (x₁ k) (x₂ k)
        = prodMat (p₁ (z k)) (q₁ (z k)) (p₂ (z k)) (q₂ (z k))
            *ᵥ prodState (x₁ (k + 1)) (x₂ (k + 1)) + prodVec (q₁ (z k)) (q₂ (z k)))
      ∧ ∀ k, prodReadout W₁ W₂ ⬝ᵥ prodState (x₁ k) (x₂ k)
          = (W₁ ⬝ᵥ x₁ k) * (W₂ ⬝ᵥ x₂ k) := by sorry

end SASAlgebra

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 trajectory-level half of part (ii), without the polynomiality of the product coefficient family.

View graph