structure LowRankUnivariateSOS.ReducedFactorization (u : UPair) : Type

ReducedFactorization u is the first half of the decomposition from \Cref{prop:decomp}: we split u = a · u₀, where a is the common factor and the reduced pair u₀ is coprime. The later files further split a into the good factor g and the peelable factor h.

• a : Poly
• u0 : UPair
• eq_scale : u = scalePair self.a self.u0
• reduced_coprime : IsCoprime self.u0.fst self.u0.snd

def LowRankUnivariateSOS.SigmaReducedNoRealRoots (u0 : UPair) : Prop

Predicate expressing the paper's statement that σ(u₀) has no real roots; compare \Cref{prop:no-real-roots}.

Equations

• LowRankUnivariateSOS.SigmaReducedNoRealRoots u0 = ∀ (x : ℝ), ¬Polynomial.IsRoot (LowRankUnivariateSOS.sigma2 u0) x

noncomputable def LowRankUnivariateSOS.gcd_sigma_decomposition (u : UPair) : ReducedFactorization u

Concrete construction of the reduced factorization u = a·u₀ by taking a = gcd(u₁,u₂). This is the formal version of the first decomposition step in \Cref{prop:decomp}. The proof is Bézout/gcd bookkeeping.

Equations

• One or more equations did not get rendered due to their size.

theorem LowRankUnivariateSOS.sigma2_not_isRoot_of_coprime (u : UPair) (hu : IsCoprime u.fst u.snd) (x : ℝ) : ¬Polynomial.IsRoot (sigma2 u) x

If u₁ and u₂ are coprime, then σ(u)=u₁²+u₂² has no real root. This is exactly the argument in \Cref{prop:no-real-roots}: a real zero of a sum of two squares forces both coordinates to vanish at that point, hence they share the linear factor X-C x, contradicting coprimality.

theorem LowRankUnivariateSOS.no_real_roots_sigma_reduced (u : UPair) (data : ReducedFactorization u) : SigmaReducedNoRealRoots data.u0

The reduced pair produced by gcd_sigma_decomposition satisfies the no-real-roots conclusion of \Cref{prop:no-real-roots}. This is an immediate corollary of the previous coprime lemma.

theorem LowRankUnivariateSOS.sigma2_isSOS (u : UPair) : IsSOS (sigma2 u)

σ(u) is itself a sum of two squares by definition. This trivial remark is used as the q ∈ Σ input to the hgroup lemma.