This paper solves the rational noncommutative analogue of Hilbert’s 17th problem: if a noncommutative rational function is positive semidefinite on all tuples of Hermitian matrices in its domain, then it is a sum of Hermitian squares of noncommutative rational functions. This result is a generalisation and culmination of earlier positivity certificates for noncommutative polynomials or rational functions without Hermitian singularities. More generally, a rational Positivstellensatz for free spectrahedra is given: a noncommutative rational function is positive semidefinite or undefined at every matricial solution of a linear matrix inequality $L\succeq 0$ if and only if it belongs to the rational quadratic module generated by L. The essential intermediate step toward this Positivstellensatz for functions with singularities is an extension theorem for invertible evaluations of linear matrix pencils.

In [12]. T. Scanlon proved a quantifier elimination result for valued D-fields in a three-sorted language by using angular component functions. Here we prove an analogous theorem in a different language which was introduced by F. Delon in her thesis. This language allows us to lift the quantifier elimination result to a one-sorted language by a process described in the Appendix. As a byproduct, we state and prove a “positivstellensatz” theorem for the differential analogue of the theory of real-series closed fields in the valued D-field setting.