noncomputable def LowRankUnivariateSOS.scalePair (g : Poly) (u : UPair) : UPair

scalePair g u is the pair obtained by multiplying both coordinates of u by the common factor g. In the paper this is the passage from u' to g u' in the h = 1 case.

Equations

• LowRankUnivariateSOS.scalePair g u = { fst := g * u.fst, snd := g * u.snd }

noncomputable def LowRankUnivariateSOS.perpPair (t : Poly) (u : UPair) : UPair

perpPair t u = (-t u₂, t u₁) is the standard syzygy orthogonal to u. It is the concrete kernel element used throughout the cone(σ(ker A_u)) arguments.

Equations

• LowRankUnivariateSOS.perpPair t u = { fst := -t * u.snd, snd := t * u.fst }

@[simp]

theorem LowRankUnivariateSOS.scalePair_fst (g : Poly) (u : UPair) : (scalePair g u).fst = g * u.fst

Coordinate formulas for scalePair, perpPair, and scalar multiplication. These are bookkeeping lemmas used to keep later polynomial identities readable.

@[simp]

theorem LowRankUnivariateSOS.scalePair_snd (g : Poly) (u : UPair) : (scalePair g u).snd = g * u.snd

@[simp]

theorem LowRankUnivariateSOS.perpPair_fst (t : Poly) (u : UPair) : (perpPair t u).fst = -t * u.snd

@[simp]

theorem LowRankUnivariateSOS.perpPair_snd (t : Poly) (u : UPair) : (perpPair t u).snd = t * u.fst

@[simp]

theorem LowRankUnivariateSOS.smul_fst (a : ℝ) (u : UPair) : (a • u).fst = a • u.fst

@[simp]

theorem LowRankUnivariateSOS.smul_snd (a : ℝ) (u : UPair) : (a • u).snd = a • u.snd

@[simp]

theorem LowRankUnivariateSOS.A_scalePair_left (g : Poly) (u v : UPair) : A (scalePair g u) v = g * A u v

The next identities record how A_u and σ interact with common factors, scalar multiples, and the perpendicular syzygy. They are the algebraic identities behind the h = 1 argument in the paper's Section \ref{sec:h=1}.

@[simp]

theorem LowRankUnivariateSOS.A_smul_right (a : ℝ) (u v : UPair) : A u (a • v) = a • A u v

@[simp]

theorem LowRankUnivariateSOS.sigma2_smul (a : ℝ) (u : UPair) : sigma2 (a • u) = a ^ 2 • sigma2 u

@[simp]

theorem LowRankUnivariateSOS.sigma2_perpPair (t : Poly) (u : UPair) : sigma2 (perpPair t u) = t ^ 2 * sigma2 u

@[simp]

theorem LowRankUnivariateSOS.sigma2_scalePair (g : Poly) (u : UPair) : sigma2 (scalePair g u) = g ^ 2 * sigma2 u

theorem LowRankUnivariateSOS.inKerA_perpPair_scalePair (g t : Poly) (u : UPair) : InKerA (scalePair g u) (perpPair t u)

The perpendicular pair (-t u₂, t u₁) lies in ker(A_{g u}). This is the explicit kernel generator behind the cone terms appearing in condition (C2).

theorem LowRankUnivariateSOS.inKerA_smul {u w : UPair} (a : ℝ) (hw : InKerA u w) : InKerA u (a • w)

The kernel is closed under real scalar multiplication. This is used when two identical kernel generators are combined into a single term by scaling with sqrt 2.

theorem LowRankUnivariateSOS.inSigmaKerCone_of_pair {u w₁ w₂ : UPair} (hw₁ : InKerA u w₁) (hw₂ : InKerA u w₂) : InSigmaKerCone u (sigma2 w₁ + sigma2 w₂)

The sum of two kernel-squares lies in cone(σ(ker(A_u))). The proof is exactly the cone bookkeeping from the paper: either keep the two generators separate, or combine equal ones using a sqrt 2 rescaling.

theorem LowRankUnivariateSOS.inSigmaKerCone_sos_mul_sigma2 (g s : Poly) (u : UPair) (hs : IsSOS s) : InSigmaKerCone (scalePair g u) (s * sigma2 u)

If s is SOS, then s·σ(u) belongs to the kernel cone of A_{g u}. This is the formal version of the paper's observation that an SOS multiple of σ(u') is generated by squares of explicit kernel vectors.

theorem LowRankUnivariateSOS.inImageA_of_isCoprime (u : UPair) (hu : IsCoprime u.fst u.snd) (q : Poly) : InImageA u q

Bézout surjectivity: if u₁ and u₂ are coprime, then every polynomial lies in im(A_u). This is the Lean incarnation of \Cref{lem:coprime_kernel} specialized to the univariate rank-2 setting.

theorem LowRankUnivariateSOS.inImageA_mul_of_isCoprime (g q : Poly) (u : UPair) (hu : IsCoprime u.fst u.snd) : InImageA (scalePair g u) (g * q)

The scaled version of Bézout surjectivity: every multiple g q lies in im(A_{g u}) when the reduced pair u is coprime.

theorem LowRankUnivariateSOS.inImagePlusSigmaKerCone_of_h1_data (g p q s : Poly) (u : UPair) (hu : IsCoprime u.fst u.snd) (hs : IsSOS s) (hp : p = g * q + s * sigma2 u) : InImagePlusSigmaKerCone (scalePair g u) p

This packages the paper's h = 1 sufficient condition. If p = g q + s σ(u) with u coprime and s SOS, then p lies in im(A_{g u}) + cone(σ(ker(A_{g u}))), which is precisely condition (C2).