theorem LowRankUnivariateSOS.factor_peeling_certificate_step {B : DotForm} (p : Poly) (u : UPair) : IsSOS p → IsSOCP B p u → ∀ (data : ReducedFactorization u), data.a ≠ 0 → ∃ (a : Poly) (g : Poly) (u0 : UPair), u = scalePair a u0 ∧ g ≠ 0 ∧ IsCoprime u0.fst u0.snd ∧ IsCoprime g (sigma2 u0) ∧ ImageOrthogonalResidual B p (scalePair a u0) (scalePair g u0)

This theorem isolates the output of the factor-peeling stage needed by the final proof: from a nonzero reduced factorization u = a·u₀, one obtains a new factor g coprime to σ(u₀) such that the residual is orthogonal to im(A_{g u₀}). This is the formal version of the transformed condition (C3) after peeling all bad factors.

theorem LowRankUnivariateSOS.rankTwo_factored_h1_setup {B : DotForm} [Fact (LinearMap.BilinMap.toQuadraticMap B).PosDef] (p : Poly) (u : UPair) : IsSOS p → IsSOCP B p u → ∃ (a : Poly) (g : Poly) (q : Poly) (s : Poly) (u0 : UPair), u = scalePair a u0 ∧ g ≠ 0 ∧ IsCoprime u0.fst u0.snd ∧ IsSOS s ∧ p = g * q + s * sigma2 u0 ∧ ImageOrthogonalResidual B p (scalePair a u0) (scalePair g u0)

This is the final reduction to the h = 1 case. It packages the proof's two main algebraic ingredients:

1. factor peeling, which produces a coprime transformed image;
2. the hgroup lemma, which writes p in the form g q + s σ(u₀). Together they yield the decomposition required by the abstract h = 1 residual-vanishing lemma.

theorem LowRankUnivariateSOS.rankTwo_no_spurious_socp {B : DotForm} [Fact (LinearMap.BilinMap.toQuadraticMap B).PosDef] (p : Poly) (u : UPair) (hp : IsSOS p) (hsocp : IsSOCP B p u) : sigma2 u = p

Main theorem, corresponding to \Cref{thm:main} specialized to the rank-2 formal model. Every SOCP of the quadratic penalty objective has zero residual, hence σ(u) = p and the point is globally optimal.

Proof sketch: reduce to rankTwo_factored_h1_setup, then invoke the abstract factored h = 1 argument from FactoredCase, which combines first-order orthogonality, second-order nonnegativity, the hgroup decomposition, and the factor-peeling transport.