70. An ellipsoidal certificate with an orientation test
On this page · Permalink · Source line 2776
Work in mass-first coordinates \(z=(m,x)\in\mathbb R\times\mathbb R^d\), with \(\lambda=(1,0,\ldots,0)\). For a center \(c\in\mathbb R^d\) and a symmetric positive definite matrix \(H\), define
Its normalized base is an ellipsoid. Set
Then \(C_{c,H}=\{z:m\geq0,\ z^{\mathsf T}Qz\geq0\}\). The cone is proper and generating, and \(m\) is strictly positive on every nonzero cone element. These facts follow by an invertible linear transformation to the Lorentz cone. In particular, an output with zero mass in the cone is the zero vector.
Let \(B_a(u)\) be polynomial operator densities on \([-1,1]\), relative to \(du/2\). Write
Proposition 62: Oriented quadratic probability certificate
Suppose that for each action and every \(u\in[-1,1]\) there are \(\tau_a(u)\geq0\) and \(R_a(u)\succeq0\) satisfying
and that
If \(z_0\in C_{c,H}\) has mass one and \(\lambda\int B_a(u)\,du/2=\lambda\), then every operator preserves \(C_{c,H}\). The supplied model has valid probabilities at every finite horizon. Polynomial sum-of-squares witnesses for the scalar inequalities and for \(R_a\) make this a finite certificate.
Read proof · Recorded Lean scope · Permalink · Source line 2800
Proof
For \(z\in C_{c,H}\), the quadratic identity gives
For a nonzero \(z\), write \(x=m(c+w)\) with \(w^{\mathsf T}Hw\leq1\). Its output mass is \(m(\beta_a+b_a^{\mathsf T}w)\). Cauchy–Schwarz in the \(H\) inner product bounds this below by
Thus both inequalities defining the desired sheet of the quadratic cone hold. The zero input causes no difficulty. Integrated mass conservation gives normalization, and induction gives the finite-horizon conclusion. For polynomial data, identities between coefficients and nonnegative sums of polynomial squares establish the displayed hypotheses throughout the interval. Terms multiplied by \(1-u^2\) are also nonnegative on that interval. \(\square\)
The orientation test is essential. The matrix \(-I\) preserves every quadratic form, but maps positive mass to negative mass. A quadratic inequality without its mass orientation can certify the wrong sheet. Likewise, testing finitely many values of \(u\) is not a substitute for a polynomial identity and its positivity witness.
This is a sufficient language, not a completeness theorem for all cones. The reference checker accepts rational scalar and matrix sum-of-squares witnesses. Its discovery routine uses the narrower conformal case \(R_a=0\), but the checker does not confuse that search restriction with the theorem's scope.