Using FindInstance to Prove No Solutions Exist

Question

For a small amount of background, I am currently working on an undergraduate research project in Combinatorial Geometry and I'm working on a case analysis for embedding spherical simplicial 2-complexes in $\mathbb{S}^2$ and looking at their properties as they relate to tuples of spheres in arbitrary sphere packings. If that made no sense, no problem.

I want to show that there does not exist a solution to the equation:

a + b + c + d + e + f + g + h + i == 16 π - 33 ArcCos[1/3] - ω

where

ω = π - 4 ArcCos[1/3] + 
2 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]]

With some bounds on $a,b,c,d,e,f,g,h,i$. I have tried inputting this into Mathematica as follows (with $\omega$ defined in a previous command)

FindInstance[
    a + b + c + d + e + f + g + h + i == 16 π - 33 ArcCos[1/3] - ω && 
    ArcCos[1/3] < a < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < b < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < c < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < d < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < e < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < f < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < g < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < h < 2 π - ArcCos[1/3] && 
    ArcCos[1/3] < i < 2 π - ArcCos[1/3], 
    {a, b, c, d, e, f, g, h, i}, Reals
]

It returns an input of {} which means that Mathematica couldn't find any solutions. This is a very good thing for me, but how can I formalize the fact that no such solutions exists other than "Mathematica couldn't find any solutions using the FindInstance command"?

Answer 1

1. If FindInstance[ expr, vars, dom] returns no instances - {}, it does not mean (in general) there are no solutions, i.e. it does not prove anything here.
2. Some kind of reasonable arguments you can get making use of Reduce, if you change the head of FindInstance[ expr, vars, dom] into Reduce[ expr, vars, dom] and evaluate it, that will return False. However this is not the unique way to proceed.
3. Since the problem is to demonstrate non-existance of solutions to the system of the equation and conditions, we can show that in a quite different way making a smart use of N.

First, let's use your ω and plug it into your equation with the following notation (L and R - respectively lhs and rhs of the equation, Cond the rest of conditions present in the problem), so we have:

ω = Pi - 4 ArcCos[1/3] + 
    2 ArcCos[(2(1/2 + 1/8(-1-3Cos[4ArcCos[1/3]])))/Sqrt[3(1-1/16(1+3Cos[4ArcCos[1/3]])^2)]];

L = a + b + c + d + e + f + g + h + i;  

R =  Simplify[16 Pi - 33 ArcCos[1/3] - ω];

Cond = 
  ( ArcCos[1/3] < a < 2 Pi - ArcCos[1/3] && ArcCos[1/3] < b < 2 Pi - ArcCos[1/3] && 
    ArcCos[1/3] < c < 2 Pi - ArcCos[1/3] && ArcCos[1/3] < d < 2 Pi - ArcCos[1/3] && 
    ArcCos[1/3] < e < 2 Pi - ArcCos[1/3] && ArcCos[1/3] < f < 2 Pi - ArcCos[1/3] && 
    ArcCos[1/3] < g < 2 Pi - ArcCos[1/3] && ArcCos[1/3] < h < 2 Pi - ArcCos[1/3] && 
    ArcCos[1/3] < i < 2 Pi - ArcCos[1/3]);

now the rhs of the equations i.e R is much nicer :

R

15 Pi - 29 ArcCos[1/3] - 2 ArcCos[2 Sqrt[2/57]]

Let's sum inequalities in the conditions to get bounds for L:

Less @@ Plus @@ List @@@ Cond // N

11.0786 < a + b + c + d + e + f + g + h + i < 45.47

as well as

Plus @@ Cond[[All, 2]] === L

True  

thus we have

11.0786 < N[L]    

and since the equation says :

L == R

we get a contradiction because

N[R]

9.05248

Thus we have no solutions at all.

Answer 2

For proving statements like this you can enter predicate logic quantifiers directly into Mathematica and let it try to Resolve the formula to a truth value.

First we state the problem ingredients

ω = FullSimplify[
      π-4 ArcCos[1/3]+2 ArcCos[(2 (1/2+1/8 (-1-3 Cos[4 ArcCos[1/3]]))) / 
      Sqrt[3 (1-1/16 (1+3 Cos[4 ArcCos[1/3]])^2)]]
    ]
vars  = {a,b,c,d,e,f,g,h,i};
eq    = Total[vars] == 16 π - 33 ArcCos[1/3] - ω //FullSimplify
conds = And @@ Thread[ ArcCos[1/3] < vars < 2 π - ArcCos[1/3] ]

and let Resolve do the work of proving

Exists[Evaluate[vars], conds, eq]

$$\exists _{\{a,\cdots,i\},\cos ^{-1}\left(\frac{1}{3}\right)<\{a,\cdots,i\}<2 \pi -\cos ^{-1}\left(\frac{1}{3}\right)}a+\cdots+i+\frac{\pi }{2}=2 \sin ^{-1}\left(2 \sqrt{\frac{2}{57}}\right)+29 \csc ^{-1}(3)$$

Resolve[%]
(* False *)

Answer 3

Just a small remark: if the variables are angles then you should probably make the bounds periodic, using something like Mod[a, 2 Pi] instead of a in the conditions. Then you obviously get solutions to this trivial problem. Here I just did it for one of the variables:

FindInstance[
 a + b + c + d + e + f + g + h + i == 
   16 Pi - 33 ArcCos[1/3] - \[Omega] && 
  ArcCos[1/3] < Mod[a, 2 Pi] < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < b < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < c < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < d < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < e < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < f < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < g < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < h < 2 Pi - ArcCos[1/3] && 
  ArcCos[1/3] < i < 2 Pi - ArcCos[1/3], {a, b, c, d, e, f, g, h, 
  i}, Reals]

(*
==> {{a -> (11 Pi)/2 - 17 ArcCos[1/3] - 
    ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
     3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  b -> (15 Pi)/4 - 8 ArcCos[1/3] - 
    1/2 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
      3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  c -> (15 Pi)/8 - 7/2 ArcCos[1/3] - 
    1/4 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
      3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  d -> (15 Pi)/16 - 5/4 ArcCos[1/3] - 
    1/8 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
      3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  e -> (15 Pi)/32 - 1/8 ArcCos[1/3] - 
    1/16 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
      3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  f -> (15 Pi)/64 + 7/16 ArcCos[1/3] - 
    1/32 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
      3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  g -> (15 Pi)/64 + 7/16 ArcCos[1/3] - 
    1/32 ArcCos[(2 (1/2 + 1/8 (-1 - 3 Cos[4 ArcCos[1/3]])))/Sqrt[
      3 (1 - 1/16 (1 + 3 Cos[4 ArcCos[1/3]])^2)]], 
  h -> -(1/2) + 2 Pi - ArcCos[1/3], i -> 1/2 + ArcCos[1/3]}}
*)

More to the point of proving statements: you should look at Resolve and its use with ForAll and Exists. This link has an example of a proof that uses Resolve.