Dependencies

The basic constructions are

They satisfy

Hence if

then

so \(s\, \sigma (u)\) lies in the cone generated by kernel squares. On the image side, coprimality gives Bézout surjectivity:

Therefore

The formal model is defined in PolynomialModel.lean and Socp.lean. For a pair of polynomials \(u=(u_1,u_2)\),

The objective is

The FOCP condition is

In Lean this is IsFOCP. The Hessian quadratic form is

The SOCP condition is the FOCP condition together with

In the kernel directions used later in the proof,

In Lean this full condition is IsSOCP.

A peeling witness is a family \(v_\eta \) satisfying

with

So the quadratic coefficient is already controlled by the previous stage, while the linear coefficient is the new target \(q\). Lean stores the local step in PeelingStepWitness and RotatedPeelingData. The recursive transport is stored in

If \(p\) and \(q\) are SOS polynomials and \(\gcd (g,q)=1\), then there exist \(s,t\) such that

Lean proves this by choosing Bézout coefficients

and defining

Then

using \(bq=1-ag\). The SOS claim for \(s\) is exactly

formalized by isSOS_mul.

Write

Then the SOCP conditions give

for the transformed image used later in the proof, and

So if one can prove

then

Evaluating the FOCP condition at \(v=u\) gives

hence

Since always \(f_p(u)\ge 0\), it follows that

This is exactly the abstract content of factored_h1_residual_eq_zero.

Assume \(a\neq 0\). Then Lean produces a factorization

such that

The peeled terminal factor is

and satisfies

Informally, each bad factor \(r_i\) is replaced by one copy of \(X^2\), while the coprime part \(g_{\mathrm{base}}\) is kept unchanged.

Assume

Then

and therefore

This is the formal \(h=1\) reduction used later by the abstract SOCP argument.

Assume one quadratic factor step

Let

and define

Then

and

Moreover,

because \(r\) divides both \(\sigma (u_0)\) and \(g_{\mathrm{start}}\). If the previous image is already orthogonal to the residual \(r_{\mathrm{res}}\), then the SOCP inequality gives

for all real \(\eta \). Hence

This is the content of dot_eq_zero_of_peeling_step; the theorem image_orthogonal_of_peeling_step upgrades it from one polynomial \(q\) to the entire next image.

Starting from

Lean builds a peeling schedule

Orthogonality propagates at each arrow by Proposition 10. Therefore the final theorem factor_peeling_image_orthogonal gives

This is the Lean form of the paper’s factor-peeling conclusion.

Lean constructs a decomposition

In Lean this is the structure ReducedFactorization produced by gcd_sigma_decomposition. The companion theorem no_real_roots_sigma_reduced proves

So the common factor of \(u_1,u_2\) is isolated in \(a\), while the reduced pair \(u_0\) is coprime and its sum of squares has no real roots.

Start from

If

then the residual vanishes directly from the SOCP inequalities. If

then factor peeling gives

Applying Lemma 7 with \(q=\sigma (u_0)\) gives

So rankTwo_factored_h1_setup returns exactly the package

For every sum-of-squares polynomial \(p\) and every second-order critical point \(u=(u_1,u_2)\) of the quadratic-penalty objective,

Equivalently,

so every SOCP is globally optimal.