Lemma 2: the admissible convolution functionals separate signals
ProvedBoydChua.gconv_separatesLemma 2 of the source. Two signals of the admissible class that differ somewhere in the past are separated by an admissible convolution functional: there is a kernel g with ∫|g|/w finite such that pairing g against the two signals gives different numbers.
The source exhibits the separating kernel explicitly. For signals u and v take g(t) = (u(t) - v(t)) w(t) e^{-t}. Its admissibility follows from the amplitude bound, since ∫|g|/w is then at most 2 M₁ times the integral of e^{-t}; and the difference of the two pairings is ∫ (u-v)² w e^{-t}, which is strictly positive because u - v is continuous and not identically zero on the half-line.
Together with the compactness of Lemma 1, this is the separating family Stone-Weierstrass requires.
import Mathlib import Definitions.Def_BoydChua open Filter Topology MeasureTheory ReservoirESN BoydChua
namespace BoydChua
theorem gconv_separates (w : ℝ → ℝ) (hw : IsWeightingC w) (M₁ M₂ : ℝ)
(hM₁ : 0 < M₁) (hM₂ : 0 < M₂)
(u v : ℝ → ℝ) (hu : SlewBdd M₁ M₂ u) (hv : SlewBdd M₁ M₂ v)
(hne : ∃ t ≥ (0:ℝ), u t ≠ v t) :
∃ g : ℝ → ℝ, AdmissibleKernel w g ∧ Gconv g u ≠ Gconv g v := by sorry
end BoydChuaRead-back
What the Lean code literally says, in plain math · claude-opus-5
Given a weighting w, positive constants M1, M2, and two slew-bounded functions that differ at at least one non-negative point, there exists a kernel admissible for w whose integral functional distinguishes them.
In words: the admissible-kernel functionals separate the points of the slew-bounded class - "points" being functions distinguished by their restriction to the non-negative half-line, which is the only thing either the class or the functionals can see.
Two points were checked independently. The separating kernel of the theory, the difference of the two signals times the weight times a decaying exponential, is genuinely admissible, measurability included: the weight is measurable because it is antitone, the signals because they are Lipschitz hence continuous, and the quotient by the weight is dominated by a constant multiple of the exponential. And a difference at a single point does suffice - but only because of the Lipschitz field: continuity propagates the difference to an open interval of positive measure, making the integral of the squared difference strictly positive. Were the Lipschitz requirement dropped, the statement would become false, since two functions differing at one point only have equal integrals against every kernel. That field, rather than the positivity of the constants, is what carries the argument.
Confirmed by the mission captain (proposal self-audit).