theorem LowRankUnivariateSOS.inKerA_of_shared_reduced {a g : Poly} {u0 w : UPair} (hg : g ≠ 0) (hker : InKerA (scalePair g u0) w) : InKerA (scalePair a u0) w

If a vector is killed by A_{g u₀} with g ≠ 0, then it is already killed by A_{a u₀} for any other scale a. This is the formal reason that kernel cone terms produced in the reduced h = 1 model can be reused for the original factorization.

theorem LowRankUnivariateSOS.factored_h1_decomposition_to_original (a g p q s : Poly) (u0 : UPair) (hg : g ≠ 0) (hcop : IsCoprime u0.fst u0.snd) (hs : IsSOS s) (hp : p = g * q + s * sigma2 u0) : ∃ (imgPart : Poly) (ws : Finset UPair), InImageA (scalePair g u0) imgPart ∧ (∀ w ∈ ws, InKerA (scalePair a u0) w) ∧ p = imgPart + ws.sum sigma2

Converts the explicit h = 1 decomposition p = g q + s σ(u₀) into the image-plus-cone form needed by the abstract SOCP argument, but now relative to the original scale a·u₀ instead of the reduced scale g·u₀.

def LowRankUnivariateSOS.ImageOrthogonalResidual (B : DotForm) (p : Poly) (u uImg : UPair) : Prop

The residual at u is orthogonal to the image of the transformed pair uImg.

Equations

• LowRankUnivariateSOS.ImageOrthogonalResidual B p u uImg = ∀ (q : LowRankUnivariateSOS.Poly), LowRankUnivariateSOS.InImageA uImg q → (B q) (LowRankUnivariateSOS.residual p u) = 0

theorem LowRankUnivariateSOS.transformed_image_plus_cone_implies_objective_eq_zero {B : DotForm} [Fact (LinearMap.BilinMap.toQuadraticMap B).PosDef] {p : Poly} {u uImg : UPair} (hsocp : IsSOCP B p u) (himg : ImageOrthogonalResidual B p u uImg) (hdecomp : ∃ (imgPart : Poly) (ws : Finset UPair), InImageA uImg imgPart ∧ (∀ w ∈ ws, InKerA u w) ∧ p = imgPart + ws.sum sigma2) : objective B p u = 0

This is the abstract certificate step behind condition (C2). If p decomposes as an image term for some transformed pair uImg plus a sum of kernel squares for the original pair u, and if the residual is orthogonal to im(A_{uImg}), then the SOCP inequalities force the objective to be zero. The proof is exactly the paper's image-plus-cone argument: the image part dies by first-order criticality, the kernel terms are nonnegative by second-order criticality, and ⟨σ(u),σ(u)-p⟩=0 closes the estimate.

theorem LowRankUnivariateSOS.factored_h1_residual_eq_zero {B : DotForm} [Fact (LinearMap.BilinMap.toQuadraticMap B).PosDef] (a g p q s : Poly) (u0 : UPair) (hg : g ≠ 0) (hcop : IsCoprime u0.fst u0.snd) (hs : IsSOS s) (hp : p = g * q + s * sigma2 u0) (himg : ImageOrthogonalResidual B p (scalePair a u0) (scalePair g u0)) (hsocp : IsSOCP B p (scalePair a u0)) : residual p (scalePair a u0) = 0

This is the factor-rescaled form of the paper's h = 1 decomposition. Starting from p = g q + s σ(u₀), it rewrites p as img(A_{g u₀}) + cone(σ(ker(A_{a u₀}))), which is the form needed by the abstract image-plus-cone lemma above.