SDP strong duality

Theorem. Fix natural numbers $n$, $nn$. Assume: a vector $c \in \mathbb{R}^n$; matrices $F_1,\dots,F_n$ and $G$, all real $nn\times nn$ and each assumed symmetric ($M^\top = M$); a point $x_s \in \mathbb{R}^n$ such that $-\big(G + \sum_i (x_s)_i F_i\big)$ is positive definite — Mathlib's positive definiteness includes the symmetry/Hermitian requirement together with $v^\top M v > 0$ for every $v \ne 0$ (for $nn = 0$ there are no nonzero vectors, so this holds vacuously); and the hypothesis that the value set

is bounded below (positive semidefiniteness likewise includes symmetry, plus $v^\top M v \ge 0$ for all $v$). Conclusion: there exists a real $nn \times nn$ matrix $Z$ such that (i) $Z$ is positive semidefinite (hence symmetric); (ii) for every $i \in \{1,\dots,n\}$, $\operatorname{tr}(F_i\, Z) + c_i = 0$, where the trace of the matrix product means $\sum_{k,\ell} (F_i)_{k\ell} Z_{\ell k}$; and (iii) $\operatorname{tr}(G\, Z) = \inf S$, an equality of real numbers with no sign flip on $\operatorname{tr}(GZ)$. Here $\inf$ is Lean's real infimum with junk value $0$ on an empty or unbounded-below set; in this statement $S$ is nonempty (it contains $c \cdot x_s$, since positive definite implies positive semidefinite) and bounded below by hypothesis, so it is the genuine infimum. No attainment of the primal infimum by a feasible $x$ is claimed, and no uniqueness of $Z$. Edge cases: for $n = 0$ the linear combination is empty and $c \cdot x = 0$, the strict-feasibility hypothesis reads "$-G$ is positive definite", condition (ii) is vacuous, and $S \subseteq \{0\}$; for $nn = 0$ all matrix conditions are vacuous and both sides of (iii) reduce to $0 = \inf S$ with $S = \{c\cdot x : x \in \mathbb{R}^n\}$.