Function Repository Resource:

PolynomialSystemInfeasibilityCertificate

Source Notebook

Find an independently verifiable certificate proving that a polynomial system has no solutions

Contributed by: Adam Strzeboński

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f₁,…,f_k},{g₁,…,g_m},vars,Reals]

finds an infeasibility certificate for the real system f₁==0∧…∧f_k==0∧g₁>=0∧…∧g_m>=0.

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f₁,…,f_k},{g₁,…,g_m},vars,Complexes]

finds an infeasibility certificate for the complex system f₁==0∧…∧f_k==0∧g₁!=0∧…∧g_m!=0.

Details

ResourceFunction["PolynomialSystemInfeasibilityCertificate"] is typically used to find an independently verifiable certificate proving that a system of real polynomial equations and inequalities does not have real solutions or a system of complex polynomial equations and inequations does not have complex solutions.

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f₁,…,f_k},{g₁,…,g_m},vars,Reals] requires {f₁,…,f_k} and {g₁,…,g_m} to be polynomials in vars with real numeric coefficients.

An infeasibility certificate for a real system has the form {{t₁,…,t_r},{u₁,…,u_k}}. Each t_i is a triple {q_i,μ_i,α_i}, where q_i is a real symmetric positive semidefinite matrix, μ_i is a list of monomials in vars, and α_i is a subset of {1,…,m}. The {u₁,…,u_k} are polynomials in vars with real numeric coefficients. Let s_i=μ_i.q_i.μ_i and

. Then s_i is non-negative for all values vars. The certificate satisfies the condition 1+∑i=1rs_iγ_i==u₁f₁+…+u_kf_k. Note that at any real solution of the system f₁==0∧…∧f_k==0∧g₁>=0∧…∧g_m>=0 we would have 1+∑i=1rs_iγ_i>=1 and u₁f₁+…+u_kf_k==0, and hence the system has no real solutions.

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f₁,…,f_k},{g₁,…,g_m},vars,Complexes] requires {f₁,…,f_k} and {g₁,…,g_m} to be polynomials in vars with numeric coefficients.

An infeasibility certificate for a complex system has the form {{u₁,…,u_k},{e₁,…,e_m}}, where {u₁,…,u_k} are polynomials in vars with numeric coefficients and {e₁,…,e_m} are non-negative integers. The certificate satisfies the condition u₁f₁+…+u_kf_k==g₁^e₁·…·g_m^e_m. Note that at any solution of the system f₁==0∧…∧f_k==0∧g₁!=0∧…∧g_m!=0 we would have u₁f₁+…+u_kf_k==0 and g₁^e₁·…·g_m^e_m!=0, and hence the system has no solutions.

Examples

Basic Examples (2)

Find an infeasibility certificate for the real system x²+y²=1 ∧ x⁴+y⁴≤1/4:

In[1]:=

$ff = {x^2 + y^2 - 1}; gg = {1/4 - x^4 - y^4}; {tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y}, Reals]$

Out[3]=

Verify that the matrices q_i are positive semidefinite:

In[4]:=

Out[4]=

Verify the condition 1+∑i=1rs_iγ_i==u₁f₁+…+u_kf_k:

In[5]:=

ss = #[[2]] . #[[1]] . #[[2]] & /@ tt;
h = 1 + ss . ((Times @@ Part[gg, #[[3]]]) & /@ tt);
Expand[h - uu . ff]

Out[6]=

Find an infeasibility certificate for the complex system x⁴+y⁴+z⁴=1 ∧ 2 x² y²+z⁴=1 ∧ x≠y ∧ x≠-y:

In[7]:=

$ff = {x^4 + y^4 + z^4 - 1, 2 x^2 y^2 + z^4 - 1}; gg = {x - y, x + y}; {uu, ee} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Complexes]$

Out[9]=

Verify the condition u₁f₁+…+u_kf_k==g₁^e₁·…·g_m^e_m:

In[10]:=

Out[10]=

We obtain a similar result by creating a new equation that forces both inequations to be False and removing the inequations:

In[11]:=

$ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ Join[ff, {x^2 - y^2 - 1}], {}, {x, y, z}, Complexes]$

Out[11]=

Scope (6)

Infeasibility certificate for a real system of equations:

In[12]:=

$ff = {x^2 + y^2 + z, z - 1}; gg = {}; {tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Reals];$

Verify correctness of the certificate:

In[13]:=

Out[13]=

In[14]:=

Out[1]=

Visualize the disjoint solution surfaces of the equations:

In[15]:=

$ContourPlot3D[{x^2 + y^2 + z == 0, z - 1 == 0}, Sequence[{x, -1, 1}, {y, -1, 1}, {z, -1, 1}, Mesh -> None, Ticks -> None, ImageSize -> Small]]$

Out[15]=

Infeasibility certificate for a real system of inequalities:

In[16]:=

$ff = {}; gg = {1 - x^2 - y^2 - z^2, 1 - (x - 2)^4 - (y - 2)^4 - z^4}; {tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Reals];$

Verify correctness of the certificate:

In[17]:=

Out[17]=

In[18]:=

Out[11]=

Visualize the disjoint solution regions of the inequalities:

In[19]:=

$RegionPlot3D[{1 - x^2 - y^2 - z^2 >= 0, 1 - (x - 2)^4 - (y - 2)^4 - z^4 >= 0}, Sequence[{x, -1, 3}, {y, -1, 3}, {z, -1, 1}, BoxRatios -> Automatic, Mesh -> None, Ticks -> None, PlotPoints -> 40, ImageSize -> Small]]$

Out[19]=

Infeasibility certificate for a real system of equations and inequalities:

In[20]:=

$ff = {x^2 + y^2 + z^2 - 1}; gg = {z^2 - 1/2, x^2 + y^2 - 2/3}; {tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Reals];$

Verify correctness of the certificate:

In[21]:=

Out[21]=

In[22]:=

Out[23]=

Visualize the disjoint solution sets of the equation and of the inequalities:

In[24]:=

$Show[{ContourPlot3D[x^2 + y^2 + z^2 - 1 == 0, Sequence[{x, -1, 1}, {y, -1, 1}, {z, -1, 1}, Ticks -> None, Mesh -> None]], RegionPlot3D[z^2 - 1/2 >= 0 && x^2 + y^2 - 2/3 >= 0, Sequence[{x, -1, 1}, {y, -1, 1}, {z, -1, 1}, PlotStyle -> Red, Ticks -> None, Mesh -> None]]}, ImageSize -> Small]$

Out[24]=

Find an infeasibility certificate for the complex system of equations:

In[25]:=

$ff = {x^2 - y, y^2 - z, x^4 - z + 1}; gg = {}; {uu, ee} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Complexes]$

Out[27]=

Verify correctness of the certificate:

In[28]:=

Out[28]=

Find an infeasibility certificate for the complex system of equations and inequations:

In[29]:=

$ff = {(x^2 - y)^2, (y^2 - z)^3}; gg = {x^4 - z}; {uu, ee} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Complexes]$

Out[31]=

Verify correctness of the certificate:

In[32]:=

Out[32]=

PolynomialSystemInfeasibilityCertificate returns unevaluated when it fails to find an infeasibility certificate:

In[33]:=

Out[33]=

In this case the system has solutions:

In[34]:=

Out[34]=

Applications (3)

Find an independently verifiable proof that surfaces x²+y²+z²=1 and x⁴+y⁴+z⁴=1/4 are disjoint:

In[35]:=

$ff = {x^2 + y^2 + z^2 - 1, x^4 + y^4 + z^4 - 1/4}; gg = {}; {tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Reals];$

Verify the proof:

In[36]:=

Out[36]=

In[37]:=

Out[39]=

Visualize the surfaces:

In[40]:=

$ContourPlot3D[{x^2 + y^2 + z^2 == 1, x^4 + y^4 + z^4 == 1/4}, Sequence[{x, -1, 1}, {y, -1, 1}, {z, -1, 1}, ContourStyle -> { Opacity[0.5], Red}, Mesh -> None, Ticks -> None, ImageSize -> Small]]$

Out[40]=

Find a proof that solids z²≥2 x²+2 y² and 16 (x²+y²)≥(x²+y²+z²+2)² are disjoint:

In[41]:=

$ff = {}; gg = {z^2 - 2 x^2 - 2 y^2, 16 (x^2 + y^2) - (x^2 + y^2 + z^2 + 2)^2}; {tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Reals];$

Verify the proof:

In[42]:=

Out[42]=

In[43]:=

Out[45]=

Visualize the solids:

In[46]:=

$RegionPlot3D[{z^2 >= 2 x^2 + 2 y^2, 16 (x^2 + y^2) >= (x^2 + y^2 + z^2 + 2)^2}, Sequence[{x, -5, 5}, {y, -5, 5}, {z, -5, 5}, Mesh -> None, Ticks -> None, PlotPoints -> 40, ImageSize -> Small]]$

Out[46]=

Find a proof that x+y+z belongs to the radical of ⟨x³+y³+z³,(x+y)² (x+z)² (y+z)²⟩:

In[47]:=

$ff = {x^3 + y^3 + z^3, (x + y)^2 (x + z)^2 (y + z)^2}; g = x + y + z; {{u, v}, {e}} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ ff, {g}, {x, y, z}, Complexes]$

Out[49]=

Verify that (x+y+z)^e==u(x³+y³+z³)+v((x+y)² (x+z)² (y+z)²):

In[50]:=

$Expand[g^e - {u, v} . ff]$

Out[50]=

Properties and Relations (4)

PolynomialSystemInfeasibilityCertificate finds an independently verifiable certificate of infeasibility:

In[51]:=

$ff = {x^8 + y^8 + z^8 - 1}; gg = {x^2 + y^2 - z^2, z - 99/100}; ({tt, uu} = ResourceFunction["PolynomialSystemInfeasibilityCertificate"][ff, gg, {x, y, z}, Reals];) // AbsoluteTiming$