theorem LowRankUnivariateSOS.isSOS_mul {p q : Poly} (hp : IsSOS p) (hq : IsSOS q) : IsSOS (p * q)

The product of two binary sums of two squares is again a binary sum of two squares. This is the classical two-squares identity, and it is the algebraic engine behind the SOS multiplier constructed in the hgroup lemma.

theorem LowRankUnivariateSOS.hgroup_affine (g p q : Poly) : IsSOS p → IsSOS q → IsCoprime g q → ∃ (s : Poly) (t : Poly), IsSOS s ∧ p = g * t + s * q

Affine hgroup lemma, corresponding to the affine version of \Cref{lem:hgroup} proved in the paper just before the projective statement. If p and q are SOS and g is coprime to q, then p can be written as g·t + s·q with s still SOS.

Proof sketch: choose Bézout coefficients a,b with a g + b q = 1; then b² p q is SOS, and a direct algebraic identity shows that g * (p * (2a - a² g)) + (b² p q) * q = p. This is the Lean compression of the paper's congruence argument modulo g.