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.