Function Repository Resource:

PolynomialSystemInfeasibilityCertificate

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

 ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f1,…,fk},{g1,…,gm},vars,Reals] finds an infeasibility certificate for the real system f1==0∧…∧fk==0∧g1>=0∧…∧gm>=0. ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f1,…,fk},{g1,…,gm},vars,Complexes] finds an infeasibility certificate for the complex system f1==0∧…∧fk==0∧g1!=0∧…∧gm!=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"][{f1,,fk},{g1,,gm},vars,Reals] requires {f1,,fk} and {g1,,gm} to be polynomials in vars with real numeric coefficients.
An infeasibility certificate for a real system has the form {{t1,,tr},{u1,,uk}}. Each ti is a triple {qi,μi,αi}, where qi is a real symmetric positive semidefinite matrix, μi is a list of monomials in vars, and αi is a subset of {1,,m}. The {u1,,uk} are polynomials in vars with real numeric coefficients. Let si=μi.qi.μi and . Then si is non-negative for all values vars. The certificate satisfies the condition 1+i=1rsiγi==u1f1++ukfk. Note that at any real solution of the system f1==0∧fk==0∧g1>=0∧gm>=0 we would have 1+i=1rsiγi>=1 and u1f1++ukfk==0, and hence the system has no real solutions.
ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{f1,,fk},{g1,,gm},vars,Complexes] requires {f1,,fk} and {g1,,gm} to be polynomials in vars with numeric coefficients.
An infeasibility certificate for a complex system has the form {{u1,,uk},{e1,,em}}, where {u1,,uk} are polynomials in vars with numeric coefficients and {e1,,em} are non-negative integers. The certificate satisfies the condition u1f1++ukfk==g1e1··gmem. Note that at any solution of the system f1==0∧fk==0∧g1!=0∧gm!=0 we would have u1f1++ukfk==0 and g1e1··gmem!=0, and hence the system has no solutions.

Examples

Basic Examples (2)

Find an infeasibility certificate for the real system x2+y2=1 ∧ x4+y4≤1/4:

 In[1]:=
 Out[3]=

Verify that the matrices qi are positive semidefinite:

 In[4]:=
 Out[4]=

Verify the condition 1+∑i=1rsiγi==u1f1++ukfk:

 In[5]:=
 Out[6]=

Find an infeasibility certificate for the complex system x4+y4+z4=1 ∧ 2 x2 y2+z4=1 ∧ x≠y ∧ x≠-y:

 In[7]:=
 Out[9]=

Verify the condition u1f1++ukfk==g1e1··gmem:

 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]:=
 Out[11]=

Scope (6)

Infeasibility certificate for a real system of equations:

 In[12]:=

Verify correctness of the certificate:

 In[13]:=
 Out[13]=
 In[14]:=
 Out[1]=

Visualize the disjoint solution surfaces of the equations:

 In[15]:=
 Out[15]=

Infeasibility certificate for a real system of inequalities:

 In[16]:=

Verify correctness of the certificate:

 In[17]:=
 Out[17]=
 In[18]:=
 Out[11]=

Visualize the disjoint solution regions of the inequalities:

 In[19]:=
 Out[19]=

Infeasibility certificate for a real system of equations and inequalities:

 In[20]:=

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]:=
 Out[24]=

Find an infeasibility certificate for the complex system of equations:

 In[25]:=
 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]:=
 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 x2+y2+z2=1 and x4+y4+z4=1/4 are disjoint:

 In[35]:=

Verify the proof:

 In[36]:=
 Out[36]=
 In[37]:=
 Out[39]=

Visualize the surfaces:

 In[40]:=
 Out[40]=

Find a proof that solids z2≥2 x2+2 y2 and 16 (x2+y2)≥(x2+y2+z2+2)2 are disjoint:

 In[41]:=

Verify the proof:

 In[42]:=
 Out[42]=
 In[43]:=
 Out[45]=

Visualize the solids:

 In[46]:=
 Out[46]=

Find a proof that x+y+z belongs to the radical of ⟨x3+y3+z3,(x+y)2 (x+z)2 (y+z)2:

 In[47]:=
 Out[49]=

Verify that (x+y+z)e==u(x3+y3+z3)+v((x+y)2 (x+z)2 (y+z)2):

 In[50]:=
 Out[50]=

Properties and Relations (4)

PolynomialSystemInfeasibilityCertificate finds an independently verifiable certificate of infeasibility:

 In[51]:=
 Out[53]=

Verify correctness of the certificate:

 In[54]:=
 Out[54]=
 In[55]:=
 Out[57]=

FindInstance usually faster proves infeasibility, but does not provide a certificate:

 In[58]:=
 Out[58]=

You can also prove infeasibility using Resolve:

 In[59]:=
 Out[59]=

Possible Issues (3)

PolynomialSystemInfeasibilityCertificate may fail even if the problem is infeasible:

 In[60]:=
 Out[60]=

This shows that x2+y2-1=0∧-x3+2 y3-2-ε>=0 is infeasible for any ε>0:

 In[61]:=
 Out[61]=

For a larger value of ε PolynomialSystemInfeasibilityCertificate succeeds:

 In[62]:=
 Out[62]=