# Using FindInstance to Prove No Solutions Exist

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"?

-
This seems like a question for math.stackexchange.com. Mathematica does not usually provide specific proofs (there is the Primality Proving Package). Surely a blank FindInstance result is in no way a proof. This question therefore becomes "how can I prove hypothesis X" which again, seems like a question for another site. –  Mr.Wizard Jul 7 '12 at 23:55
You could try to recast as linear (weak) inequalities over the rationals by slightly enlarging the bounds. If FindInstance/Reduce give no solutions to that, then there are no solutions. –  Daniel Lichtblau Jul 8 '12 at 1:12
@DanielLichtblau Can you explain further? Why? (thanks) –  belisarius Jul 8 '12 at 16:06
@Belisarius Linear programming over the rationals is fairly stable technology. It could have bugs, I guess. But that's not too likely. Reduce and FindInstance will use LP under the hood, if presented with a problem falling into that category. The one above does so, if i am seeing it correctly. –  Daniel Lichtblau Jul 8 '12 at 22:10

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


N[R]

9.05248


Thus we have no solutions at all.

-

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 *)

-
Nice and +1, anyway this should be corrected \\FullSimplify in eq to //FullSimplify or //Simplify. –  Artes Jul 12 '12 at 7:43
oh yes, thanks for pointing that out. –  Thies Heidecke Jul 12 '12 at 18:53
@ThiesHeidecke: I ended up having already solved this particular problem I asked in the question, but this technique happened to end up being very useful for something else I am now working on, so thank you! –  Samuel Reid Jul 13 '12 at 3:34
That's good to hear, you're welcome! –  Thies Heidecke Jul 13 '12 at 18:06

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.

-
I'm not sure why I should add my bounds on the angles to be periodic... I only consider it relevant to consider to internal angle which is bounded below $2\pi$. –  Samuel Reid Jul 8 '12 at 9:21