The S-procedure (losslessness)

Proved

ConvexOptimization.s_procedure

by Shuze Chen · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-optimizations-proceduresemidefinite-programming

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

q_k(x) \;=\; x^{T}F_k x + 2 g_k^{T} x + h_k \qquad (k = 1, 2),

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

\bigl(q_1(x) \le 0 \Rightarrow q_2(x) \le 0 \ \text{ for every } x \in \mathbb{R}^n\bigr) \qquad\Longleftrightarrow\qquad \exists\, \lambda \ge 0 : \ \lambda M_1 - M_2 \;\succeq\; 0 .

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.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_quadraticForms

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.s_procedure {nn : ℕ}
    (F₁ F₂ : Matrix (Fin nn) (Fin nn) ℝ) (hF₁ : F₁.IsSymm) (hF₂ : F₂.IsSymm)
    (g₁ g₂ : Fin nn → ℝ) (h₁ h₂ : ℝ)
    (xh : Fin nn → ℝ) (hxh : quadForm F₁ g₁ h₁ xh < 0) :
    (∀ x, quadForm F₁ g₁ h₁ x ≤ 0 → quadForm F₂ g₂ h₂ x ≤ 0) ↔
      ∃ lam : ℝ, 0 ≤ lam ∧
        (lam • symQuadBlock F₁ g₁ h₁ - symQuadBlock F₂ g₂ h₂).PosSemidef := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 655, 657-658, §B.2 eq. (B.6)-(B.7) (the S-procedure for a single quadratic constraint), proof in §B.4

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Theorem. Fix a natural number $nn$ ; real $nn\times nn$ matrices $F_1$ , $F_2$ , each assumed symmetric; vectors $g_1, g_2 \in \mathbb{R}^{nn}$ ; scalars $h_1, h_2 \in \mathbb{R}$ ; and a point $x_h \in \mathbb{R}^{nn}$ with $q_1(x_h) < 0$ (strict feasibility of the first quadratic), where the file's ConvexOptimization_quadForm unfolds as $q_k(x) := x^\top F_k x + 2\,(g_k \cdot x) + h_k$ (factor $2$ on the linear term). No convexity or definiteness is assumed of $F_1$ or $F_2$ . The theorem asserts the equivalence:

\Big(\forall x \in \mathbb{R}^{nn}:\ q_1(x) \le 0 \implies q_2(x) \le 0\Big) \iff \Big(\exists\, \lambda \in \mathbb{R}:\ 0 \le \lambda \ \wedge\ \lambda\, M_1 - M_2 \text{ is positive semidefinite}\Big),

where, unfolding the file's ConvexOptimization_symQuadBlock, $M_k$ is the $(nn+1)\times(nn+1)$ block matrix over the index type $\mathrm{Fin}\,nn \oplus \mathrm{Unit}$ ( $nn$ coordinates plus one extra index)

M_k = \begin{pmatrix} F_k & g_k \\ g_k^\top & h_k \end{pmatrix}.

Note the exact orientation of the matrix condition: $\lambda$ multiplies $M_1$ and $M_2$ is subtracted, i.e. $\lambda M_1 \succeq M_2$ in Loewner order; both implications relating $q_1 \le 0$ and $q_2 \le 0$ are nonstrict, and $\lambda \ge 0$ is nonstrict. Positive semidefiniteness in Mathlib includes the symmetry requirement (satisfied here since $F_1, F_2$ are symmetric). Edge case: for $nn = 0$ everything is scalar — the hypothesis forces $h_1 < 0$ , and the statement reads $(h_1 \le 0 \implies h_2 \le 0) \iff \exists \lambda \ge 0,\ \lambda h_1 - h_2 \ge 0$ , i.e. $h_2 \le 0$ on the left.

Human review

Endorsed by Community (Bot) · Aug 13, 2026
Endorsed by Shuze Chen · Aug 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph