The S-procedure (losslessness)

The S-procedure — the goal of this mission: one quadratic inequality implies another exactly when a single nonnegative multiplier certifies it.

Let $F_1, F_2$ be symmetric $n \times n$ real matrices, $g_1, g_2 \in \mathbb{R}^n$, $h_1, h_2 \in \mathbb{R}$, and set

with associated block matrices $M_k = \begin{bmatrix} F_k & g_k \\ g_k^{T} & h_k\end{bmatrix}$. Assume the strict-feasibility (Slater) condition: some $\hat{x}$ satisfies $q_1(\hat{x}) < 0$. Then

The right-hand side is a linear matrix inequality in $\lambda$, so an implication between two quadratic inequalities — a statement quantified over all of $\mathbb{R}^n$, and in general nonconvex — becomes a small semidefinite feasibility problem. The direction $\Leftarrow$ is elementary; it is the converse, losslessness, that is the theorem, and it holds only for a pair of quadratics: with two or more constraints the analogous procedure is merely sufficient.

Known as the S-procedure in control, where it certifies stability and dissipativity of systems with quadratic constraints, the result is also the exactness statement behind trust-region subproblems and behind robust optimization with ellipsoidal uncertainty — one of the very few nonconvex problems with a provably zero duality gap.

Formalization Note The quadratics and their block matrices are the mission's quadForm and symQuadBlock; the certificate is PosSemidef of lam • symQuadBlock F₁ g₁ h₁ - symQuadBlock F₂ g₂ h₂. Strict feasibility is a hypothesis of the whole iff, matching the book. Source: B&V §B.2, p. 655, proved in §B.4, pp. 657–658.