Theorem 1: approximation by a bank of linear filters and a polynomial readout
ProvedBoydChua.solutionTheorem 1 of the source, the headline result. Let a tolerance be given and let N be any time-invariant operator with fading memory on the class of amplitude- and slew-bounded signals. Then there are finitely many admissible kernels and a polynomial such that the operator sending a signal to the polynomial evaluated on its convolutions against those kernels approximates N to within the tolerance — simultaneously for every admissible signal and at every instant.
That is a bank of linear filters followed by a polynomial readout: the architecture of Fig. 3 of the source, and recognisably the architecture of a reservoir computer.
The statement is given in this form rather than as an explicit Volterra kernel expansion. Expanding a polynomial in convolutions into Volterra kernels is a purely algebraic restatement — the source performs it in its Section V — and formalising Volterra kernels would add bookkeeping without adding mathematical content.
What makes the result non-classical is the domain of uniformity. The approximation holds over the whole infinite time horizon and over the entire admissible class at once, and that class is not compact for the supremum norm. The proof supplied by the source is Stone-Weierstrass applied on the weighted-norm compact set of Lemma 1, with the separating family of Lemma 2, followed by time invariance to carry the present-time estimate to every instant.
import Mathlib import Definitions.Def_BoydChua open Filter Topology MeasureTheory ReservoirESN BoydChua
namespace BoydChua
theorem solution (M₁ M₂ : ℝ) (hM₁ : 0 < M₁) (hM₂ : 0 < M₂)
(w : ℝ → ℝ) (hw : IsWeightingC w)
(N : (ℝ → ℝ) → (ℝ → ℝ)) (hTI : IsTimeInvariantC N)
(hFM : PointwiseFMPC (fun u => N u 0) M₁ M₂ w) (ε : ℝ) (hε : 0 < ε) :
∃ (m : ℕ) (g : Fin m → (ℝ → ℝ)) (p : MvPolynomial (Fin m) ℝ),
(∀ i, AdmissibleKernel w (g i)) ∧
∀ u, SlewBdd M₁ M₂ u → ∀ r ≥ (0:ℝ),
|N u r - MvPolynomial.eval (fun i => Gconv (g i) (ShiftC r u)) p| ≤ ε := by sorry
end BoydChuaRead-back
What the Lean code literally says, in plain math · claude-opus-5
Given positive M1, M2, a weighting w, an operator on real functions that is time-invariant for non-negative shifts and whose instant-zero functional has the fading-memory property on the slew-bounded class, and a positive tolerance e, there exist an integer m, m kernels all admissible for w, and a polynomial in m variables - all chosen independently of the input and of the time - such that for every slew-bounded input and every non-negative r, the output at r differs by at most e from the polynomial evaluated on the m pairings of the kernels against the input shifted by r.
That is, the operator is uniformly approximated over its whole input class and over all non-negative times by a polynomial in finitely many weighted integrals of the time-shifted input: a bank of linear filters followed by a polynomial readout.
The junction between the time-invariance hypothesis and the conclusion was checked to be exact: the shift by a non-negative amount preserves the slew-bounded class, whereas it provably does not for a negative amount, and both the hypothesis and the conclusion restrict to non-negative shifts, so the two domains coincide with no gap.
Confirmed by the mission captain (proposal self-audit).