59. A finite certificate over an entire observation interval
On this page · Permalink · Source line 2316
Specialize to \(Y=[-1,1]\) and \(\mu(du)=du/2\). Suppose \(B_a(u)\) is a matrix polynomial. A finite congruence certificate can prove positivity for every \(u\), not merely for values on a grid.
For a real \(d^2\times d^2\) symmetric matrix \(F\), define
Vectorization orders the pairs with output index first inside each input column. If
then \(\Phi_F(X)=\sum_\nu w_\nu K_\nu X K_\nu^{\mathsf T}\). Every positive semidefinite \(F\) has a real factorization of this kind. The matrix is the usual Choi/Gram representation, with an explicit index convention [R16].
Proposition 53: Polynomial Gram certificate for interval observations
Fix the injective embedding \(\mathcal J\) and its strict interior witness from Proposition 50. Set
Suppose each action has constant positive semidefinite matrices \(G_{a,0},G_{a,1}\), with the second term omitted when \(q=0\), such that
Assume also \(z_0\in K_{\mathcal J}\) and the exact integrated mass identity. Then the model is internally probability-valid for every observation value in \([-1,1]\) and every finite horizon. The intertwining condition is finitely many coefficient equalities. The normalization condition uses only
Read proof · Recorded Lean scope · Permalink · Source line 2335
Proof
Both Gram expressions are positive semidefinite on the interval because \(1-u^2\geq0\) there. Factoring \(F_a(u)\) at a fixed \(u\) gives a positive congruence map, whether or not its individual factors depend polynomially on \(u\). The intertwining identity therefore proves \(B_a(u)C_{\mathcal J}\subseteq C_{\mathcal J}\). Polynomials on a compact interval are integrable. The mass identity and Proposition 52 prove the assertion. Equality of two finite matrix polynomials is equivalent to equality of every coefficient. The moment values follow by elementary integration. \(\square\)
For fixed \(\mathcal J\) and fixed degree bounds, unknown entries of \(B_a\) and the Gram matrices obey linear equalities and positive semidefinite constraints. A convex data-fit objective therefore gives a semidefinite feasibility or optimization problem in this fixed representation. Jointly choosing \(\mathcal J\) changes the problem: the intertwining equation then contains products of unknown coefficients.
This is a sufficient certificate, not a completeness theorem for all positive kernels or all curved domains. A negative answer at one degree is not a proof of model invalidity. Approximate Gram feasibility is also not an exact witness. Rational factorizations with nonnegative rational weights, or rigorous matrix-positivity bounds, must survive a separate replay.
The reference checker accepts a factored version:
It checks the polynomial identities, weights, support, embedding, initial state and normalization exactly. It does not run a general semidefinite optimizer. The operator identity holds on the image of \(\mathcal J\); trace preservation of an arbitrary extension outside that image is not required.