Riccati Stability Without Auxiliary Matrices
Jeffrey Humpherys
math.OC
Sep 5, 2026 · v2
eess.SY math.FA math.SP
TL;DR
The main results of Sections 2–4, including the worked example's identities, are formalized and checked in Lean 4 with Mathlib (with Claude's assistance), with a Zenodo artifact.
Abstract
In the 2004 collection Unsolved Problems in Mathematical Systems and Control Theory, Erik Verriest posed the problem of characterizing Riccati stability “without invoking additional matrices.” We give such a characterization through a scalar invariant of the resolvent family. The invariant is defined by covariance balances using at most $n^2+1$ frequency–direction pairs. A finite-dimensional separation argument shows that this covariance radius equals the optimal common ellipsoidal norm of the resolvent family. Combined with the strict bounded real lemma, this yields a necessary and sufficient condition for Riccati stability involving only the Hurwitz property of the first matrix and a single scalar inequality. The invariant reduces to the ordinary spectral radius for one matrix, lies between the pointwise spectral-radius and unscaled small-gain levels of the resolvent family, and coincides with the operator-space spectral radius of Shalit and Shamovich for the natural resolvent function space. The main results have been formally verified in the Lean proof assistant.
Problem
Verriest asked for a characterization of Riccati stability of linear delay systems (A,B) that does not invoke auxiliary positive-definite matrices P and Q. Lyapunov's theorem achieves this kind of elimination in the delay-free case.
Approach
The paper defines a covariance radius of a compact matrix family through covariance balances over at most n^2+1 matrix–direction pairs. A finite-dimensional separation argument, using Carathéodory's theorem, shows that this radius equals the optimal common ellipsoidal norm. Applied to the resolvent family G_{A,B}(ω) and combined with the strict bounded real lemma, it gives a scalar criterion. The results were formalized in Lean 4 with Mathlib.
Results
(A,B) is Riccati-stable if and only if A is Hurwitz and ρ_R(A,B)<1. The invariant lies between the pointwise spectral-radius and small-gain levels, and coincides with the Shalit–Shamovich operator-space spectral radius. A 2×2 example is strongly delay-independent stable but not Riccati-stable.
