Maple Program for MC 2021 Paper: a Machine Proof of an Inequality for the Sum of Distances between Four Points on the Unit Hemisphere using Maple Software

EasyChair Preprint no. 6349

26 pagesDate: August 23, 2021

Abstract

In this document, we present the Maple program for our
Maple Conference 2021 paper, where we proved a geometrical inequality
which states that for any four points on the unit hemisphere, the largest
sum of distances between the points is $4+4\sqrt{2}$ using Maple computation.
In our proof, we have constructed a rectangular neighborhood of the local
maximum point in the feasible set, which size is explicitly determined,
and proved that (1): the objective function is bounded by a quadratic
polynomial which takes the local maximum point as the unique critical
point in the neighbor- hood, and (2): the rest part of the feasible set can
be partitioned into a finite union of a large number of very small cubes
so that on each small cube the conjecture can be verified by estimating
the objective function with exact numerical computation. The attched
Maple program is for the second part. The work on first part, i.e., the
construction of the critical neighborhood, has been published recently in
the ADG 2021 (the Thirteenth International Conference on Automated
Deduction in Geometry), where we have proved that the sum of distances
between points contained in the constructed neighborhoods is not larger
than $4+4\sqrt{2}$, also using Maple computatin.

Keyphrases: Branch and Bound, computational geometry, global search algorithm, inequality, Maple program