Summary. This part of this book, which is the first of the four foundational chapters, presents a systematic development of trigonometry, volume, hypermap, and fan. There is a separate chapter on each of these topics. The purpose of the this material is to build a bridge between the foundations of mathematics, as presented in formal theorem proving systems such as HOL Light, and the solution to the packing problem.

In this chapter, trigonometry is developed analytically. Basic trigonometric functions are defined by their power series representations, and calculus of a single real variable is used to develop the basic properties of these functions. Basic vector geometry is presented.

Background Knowledge

formal proof

We repeat that our purpose is to give a blueprint of the formal proof of Kepler's conjecture that no packing of congruent balls in three-dimensional Euclidean space has density greater than the familiar cannonball packing. The blueprint of a formal proof is not the same as a formal proof, which is a fleeting pattern of bits in a computer. The book describes to the reader how to construct the computer code that produces and then reliably reproduces that pattern of bits.

A more traditional book might take as its starting point the imagined mathematical background of a typical reader. The blueprint of a formal proof starts instead with the current mathematical background of a formal proof assistant. I surveyed the knowledge base of my formal proof assistant and compared it with what is needed in the construction of our formal proof. It turns out that the proof assistant already has an adequate background in real analysis, basic topology, and plane trigonometry, including the trigonometric addition laws, and formulas for derivatives.