# Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

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

Contributed by:
Adam Strzeboński

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{ finds an infeasibility certificate for the real system | |

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{ finds an infeasibility certificate for the complex system |

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*_{1},…,*f*_{k}},{*g*_{1},…,*g*_{m}},*vars*,Reals] requires {*f*_{1},…,*f*_{k}} and {*g*_{1},…,*g*_{m}} to be polynomials in *vars* with real numeric coefficients.

An infeasibility certificate for a real system has the form {{*t*_{1},…,*t*_{r}},{*u*_{1},…,*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*_{1},…,*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*=1*r**s*_{i}*γ*_{i}==*u*_{1}*f*_{1}+…+*u*_{k}*f*_{k}. Note that at any real solution of the system *f*_{1}==0∧…∧*f*_{k}==0∧*g*_{1}>=0∧…∧*g*_{m}>=0 we would have 1+∑*i*=1*r**s*_{i}*γ*_{i}>=1 and *u*_{1}*f*_{1}+…+*u*_{k}*f*_{k}==0, and hence the system has no real solutions.

ResourceFunction["PolynomialSystemInfeasibilityCertificate"][{*f*_{1},…,*f*_{k}},{*g*_{1},…,*g*_{m}},*vars*,Complexes] requires {*f*_{1},…,*f*_{k}} and {*g*_{1},…,*g*_{m}} to be polynomials in *vars* with numeric coefficients.

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

Find an infeasibility certificate for the real system x^{2}+y^{2}=1 ∧ x^{4}+y^{4}≤1/4:

In[1]:= |

Out[3]= |

Verify that the matrices *q*_{i} are positive semidefinite:

In[4]:= |

Out[4]= |

Verify the condition 1+∑*i*=1*r**s*_{i}*γ*_{i}==*u*_{1}*f*_{1}+…+*u*_{k}*f*_{k}:

In[5]:= |

Out[6]= |

Find an infeasibility certificate for the complex system x^{4}+y^{4}+z^{4}=1 ∧ 2 x^{2} y^{2}+z^{4}=1 ∧ x≠y ∧ x≠-y:

In[7]:= |

Out[9]= |

Verify the condition *u*_{1}*f*_{1}+…+*u*_{k}*f*_{k}==*g*_{1}^{e1}·…·*g*_{m}^{em}:

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]= |

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]= |

Find an independently verifiable proof that surfaces x^{2}+y^{2}+z^{2}=1 and x^{4}+y^{4}+z^{4}=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 z^{2}≥2 x^{2}+2 y^{2} and 16 (x^{2}+y^{2})≥(x^{2}+y^{2}+z^{2}+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 ⟨x^{3}+y^{3}+z^{3},(x+y)^{2} (x+z)^{2} (y+z)^{2}⟩:

In[47]:= |

Out[49]= |

Verify that (x+y+z)^{e}==u(x^{3}+y^{3}+z^{3})+v((x+y)^{2} (x+z)^{2} (y+z)^{2}):

In[50]:= |

Out[50]= |

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]= |

PolynomialSystemInfeasibilityCertificate may fail even if the problem is infeasible:

In[60]:= |

Out[60]= |

This shows that x^{2}+y^{2}-1=0∧-x^{3}+2 y^{3}-2-ε>=0 is infeasible for any ε>0:

In[61]:= |

Out[61]= |

For a larger value of ε PolynomialSystemInfeasibilityCertificate succeeds:

In[62]:= |

Out[62]= |

- 1.0.0 – 10 January 2022

This work is licensed under a Creative Commons Attribution 4.0 International License