Dines's theorem: vector witness for PSD averages of two quadratic forms

Proved

ConvexOptimization.field_of_values_psd_witness

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

convex-optimizations-proceduresemidefinite-programming

Hidden convexity of the joint range of two quadratic forms: any value attained by a positive semidefinite matrix is attained by a rank-one one.

Let $A, B$ be symmetric $n \times n$ real matrices and let $X$ be positive semidefinite. Then there exists a single vector $x \in \mathbb{R}^n$ with

x^{T} A x \;=\; \operatorname{tr}(AX), \qquad x^{T} B x \;=\; \operatorname{tr}(BX).

Equivalently, the set $\{(x^{T}Ax,\, x^{T}Bx) : x \in \mathbb{R}^n\} \subseteq \mathbb{R}^2$ — the joint range of the pair — already contains everything the larger set $\{(\operatorname{tr}(AX), \operatorname{tr}(BX)) : X \succeq 0\}$ contains, so the semidefinite relaxation of a pair of quadratic forms is exact.

This is the precise reason the S-procedure is lossless: the proof relaxes a pair of quadratic inequalities to a semidefinite program, and this statement converts a matrix solution of the relaxation back into a genuine vector. It is a two-form phenomenon — for three or more quadratic forms the analogous statement fails, and the S-procedure acquires a gap.

Formalization Note The conclusion is an existential over x : Fin n → ℝ with both quadratic values written using ⬝ᵥ and Matrix.mulVec, and X.PosSemidef in Mathlib already carries Hermitian-ness. The book proves it by induction on the rank of $X$ . Source: B&V §B.3, p. 656, eq. (B.8).

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.field_of_values_psd_witness {nn : ℕ}
    (A B : Matrix (Fin nn) (Fin nn) ℝ) (hA : A.IsSymm) (hB : B.IsSymm)
    (X : Matrix (Fin nn) (Fin nn) ℝ) (hX : X.PosSemidef) :
    ∃ x : Fin nn → ℝ,
      x ⬝ᵥ A.mulVec x = (A * X).trace ∧ x ⬝ᵥ B.mulVec x = (B * X).trace := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 656, §B.3 eq. (B.8) (the set W(A,B); every value attained by a PSD matrix on a pair of quadratic forms is attained by a rank-one one)

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 $A$ and $B$ , each assumed symmetric; and a real $nn\times nn$ matrix $X$ assumed positive semidefinite (which in Mathlib includes the symmetry requirement together with $v^\top X v \ge 0$ for all $v$ ). Conclusion: there exists a single vector $x \in \mathbb{R}^{nn}$ satisfying both equalities simultaneously:

x^\top A x = \operatorname{tr}(A X) \quad\text{and}\quad x^\top B x = \operatorname{tr}(B X),

where $x^\top M x = \sum_{i,j} x_i M_{ij} x_j$ and $\operatorname{tr}(MX) = \sum_{k,\ell} M_{k\ell} X_{\ell k}$ . Exactly two matrices $A, B$ are matched (a pair, not an arbitrary family), the equalities are exact (not inequalities), no normalization is imposed on $X$ (its trace and rank are arbitrary), and no constraint (such as unit norm) is placed on the witness $x$ . Edge case: for $nn = 0$ the only vector is the empty one and all four quantities are $0$ , so the statement holds trivially.

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