The rank-2 polynomial model

This file and Socp.lean define the formal model behind the main theorem. The statement-level definitions below (Poly, UPair, sigma2, A, residual, IsSOS) are duplicated verbatim in the root module Challenge.lean, which is the statement surface audited by the Palomar registry. Palomar's Comparator requires the two copies to elaborate to identical terms, so the import list of this file must stay equal to the import list of Challenge.lean, and the duplicated definitions must not be edited in one place without the other.

@[reducible, inline]

abbrev LowRankUnivariateSOS.Poly : Type

Equations

• LowRankUnivariateSOS.Poly = Polynomial ℝ

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.instGCDMonoidPoly : GCDMonoid Poly

Equations

• LowRankUnivariateSOS.instGCDMonoidPoly = EuclideanDomain.gcdMonoid LowRankUnivariateSOS.Poly

structure LowRankUnivariateSOS.UPair : Type

UPair is the rank-2 factor variable \vec u = (u₁,u₂) from the paper. We work throughout with pairs because the paper's proof of the no-spurious-SOCP theorem treats the case r = 2, the Pythagoras number of univariate polynomials; this development formalizes exactly that case.

• fst : Poly
• snd : Poly

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.instDecidableEqUPair : DecidableEq UPair

Equations

• LowRankUnivariateSOS.instDecidableEqUPair = inferInstance

theorem LowRankUnivariateSOS.UPair.ext {u v : UPair} (hfst : u.fst = v.fst) (hsnd : u.snd = v.snd) : u = v

Extensionality for polynomial pairs. This is the basic way we identify two candidate factorizations once their two coordinates agree.

theorem LowRankUnivariateSOS.UPair.ext_iff {u v : UPair} : u = v ↔ u.fst = v.fst ∧ u.snd = v.snd

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.UPair.instZero : Zero UPair

Equations

• LowRankUnivariateSOS.UPair.instZero = { zero := { fst := 0, snd := 0 } }

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.UPair.instAdd : Add UPair

Equations

• LowRankUnivariateSOS.UPair.instAdd = { add := fun (u v : LowRankUnivariateSOS.UPair) => { fst := u.fst + v.fst, snd := u.snd + v.snd } }

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.UPair.instNeg : Neg UPair

Equations

• LowRankUnivariateSOS.UPair.instNeg = { neg := fun (u : LowRankUnivariateSOS.UPair) => { fst := -u.fst, snd := -u.snd } }

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.UPair.instSub : Sub UPair

Equations

• LowRankUnivariateSOS.UPair.instSub = { sub := fun (u v : LowRankUnivariateSOS.UPair) => { fst := u.fst - v.fst, snd := u.snd - v.snd } }

@[implicit_reducible]

noncomputable instance LowRankUnivariateSOS.UPair.instSMulReal : SMul ℝ UPair

Equations

• LowRankUnivariateSOS.UPair.instSMulReal = { smul := fun (a : ℝ) (u : LowRankUnivariateSOS.UPair) => { fst := a • u.fst, snd := a • u.snd } }

noncomputable def LowRankUnivariateSOS.sigma2 (u : UPair) : Poly

The quadratic map σ(\vec u) = u₁² + u₂² from the paper. This is the SOS polynomial represented by the rank-2 factor u.

Equations

• LowRankUnivariateSOS.sigma2 u = u.fst ^ 2 + u.snd ^ 2

noncomputable def LowRankUnivariateSOS.A (u v : UPair) : Poly

The linear map A_u(v) = u₁ v₁ + u₂ v₂ introduced in the paper before Definition \ref{def:socp}. It packages the first-order variation of σ.

Equations

• LowRankUnivariateSOS.A u v = u.fst * v.fst + u.snd * v.snd

noncomputable def LowRankUnivariateSOS.residual (p : Poly) (u : UPair) : Poly

The primal residual σ(u) - p. Vanishing of this residual is exactly the statement that u is a global minimizer for the polynomial p.

Equations

• LowRankUnivariateSOS.residual p u = LowRankUnivariateSOS.sigma2 u - p

def LowRankUnivariateSOS.IsSOS (p : Poly) : Prop

IsSOS p is the concrete rank-2 SOS representation used in the paper: p = q₁² + q₂². Since every nonnegative univariate polynomial is a sum of two squares, this is the right notion of feasibility for the main theorem.

Equations

• LowRankUnivariateSOS.IsSOS p = ∃ (q₁ : LowRankUnivariateSOS.Poly) (q₂ : LowRankUnivariateSOS.Poly), p = q₁ ^ 2 + q₂ ^ 2

def LowRankUnivariateSOS.InImageA (u : UPair) (q : Poly) : Prop

Membership in the image of A_u. In the paper this is the condition q ∈ im(A_u).

Equations

• LowRankUnivariateSOS.InImageA u q = ∃ (v : LowRankUnivariateSOS.UPair), LowRankUnivariateSOS.A u v = q

def LowRankUnivariateSOS.InKerA (u v : UPair) : Prop

Membership in the kernel of A_u. In the paper this is v ∈ ker(A_u).

Equations

• LowRankUnivariateSOS.InKerA u v = (LowRankUnivariateSOS.A u v = 0)

def LowRankUnivariateSOS.InSigmaKerCone (u : UPair) (q : Poly) : Prop

Membership in the cone generated by σ(ker(A_u)). This is the cone term in the paper's sufficient condition (C2): im(A_u) + cone(σ(ker(A_u))).

Equations

• LowRankUnivariateSOS.InSigmaKerCone u q = ∃ (ws : Finset LowRankUnivariateSOS.UPair), (∀ w ∈ ws, LowRankUnivariateSOS.InKerA u w) ∧ q = ws.sum LowRankUnivariateSOS.sigma2