Just a minor remark on the terminology:

Historically, the result known as S-procedure was related to quadratic functions (as discussed, for example, in Sec. 2.6.3 of the freely online available Boyd, Stephen, Laurent El Ghaoui, Eric Feron, and Venkataramanan Balakrishnan. Linear Matrix Inequalities in System and Control Theory. Studies in Applied and Numerical Mathematics. Society for Industrial and Applied Mathematics, 1994, https://web.stanford.edu/~boyd/lmibook/).

The extension to SOS polynomials is (perhaps better) known as Putinar’s Positivstellensatz (as discussed, for example, in Sec. 2.4 in J. B. Lasserre, An Introduction to Polynomial and Semi-Algebraic Optimization. in Cambridge Texts in Applied Mathematics Book, no. 52. Cambridge: Cambridge University Press, 2015).

It may help readers when searching for some more info in the literature.

Stabilizability of (A,B) is not enough to guarantee uniqueness of the "good" solution to ARE. Detectability of the artificial system (A,sqrt(Q)) must also be satisfied to guarantee existence of a unique positive semidefinite S that stabilises the system. If positive definiteness of S is required, then (A,sqrt(Q)) must be observable.