Flyspeck II [Elektronische Ressource] : the basic linear programs / Steven Obua

f
f f f
f f f f
f f
f f f
f f f f
f f f
Flyspeck II: The Basic Linear Programs
StevenObua
Lehrstuhlfur¨ Software&SystemsEngineering
Institutfur¨ Informatik
TechnischeUniversitat¨ Munchen¨Lehrstuhlfur¨ Software&SystemsEngineering
Institutfur¨ Informatik
TechnischeUniversitat¨ Munchen¨
Flyspeck II: The Basic Linear Programs
StevenObua
Vollstandiger¨ Abdruck der von der Fakultat¨ fur¨ Informatik der Technischen
Universitat¨ Munchen¨ zurErlangungdesakademischenGradeseines
DoktorsderNaturwissenschaften(Dr.rer.nat.)
genehmigtenDissertation.
Vorsitzender: Univ. Prof.Dr.ThomasHuckle
Prufer¨ derDissertation: 1.Univ. Prof.TobiasNipkow,Ph.D.
2.Prof.ThomasC.Hales
UniversityofPittsburgh/USA
Die Dissertation wurde am 31. Januar 2008 bei der Technischen Universitat¨
Munchen¨ eingereicht und durch die Fakultat¨ fur¨ Informatik am 8. Mai 2008 ange
nommen.ToFrankFeuerstein,
whowasthefirsttoteachme
whatmathematicsisallabout.Contents
1 Introduction 1
2 TheHOLComputingLibrary 3
2.1 WhatistheHCL? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.2 ArithmeticinCommutativeRingswithUnity . . . . . . . . . . . . . . 4
2.3 PerformanceShowdown: Factorials . . . . . . . . . . . . . . . . . . . 8
2.4 ControllingEvaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.4.1 ConditionalRules. . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.4.2 StrictorLazyEvaluation? . . . . . . . . . . . . . . . . . . . . . 11
2.5 ModesoftheHCL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.5.1 AnAbstractMachineInterface . . . . . . . . . . . . . . . . . . 13
2.5.2 TheBarras . . . . . . . . . . . . . . . . . . . . . . . . 16
2.5.3 TheSMLMachine . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.5.4 TheHaskell . . . . . . . . . . . . . . . . . . . . . . . . 33
2.6 TheHCLCokernel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.6.1 ABird’s EyeViewoftheIsabelleKernel . . . . . . . . . . . . . 33
2.6.2 RemovingandAttachingTypes . . . . . . . . . . . . . . . . . . 36
2.6.3 ComputingEquations . . . . . . . . . . . . . . . . . . . . . . . 37
2.6.4 MixingModusPonens,Instantiation,andComputation. . . . 39
2.6.5 PolymorphicLinking . . . . . . . . . . . . . . . . . . . . . . . . 40
3 ProvingBoundsforRealLinearPrograms 41
3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.2 TheBasicIdea . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.2.1 ReducingthecaseM=−∞tothecase−∞<M<∞ . . . . . . 43
3.2.2 Thecase−∞<M<∞ . . . . . . . . . . . . . . . . . . . . . . . 44
3.3 FiniteMatrices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.3.1 DimensionofaFiniteMatrix . . . . . . . . . . . . . . . . . . . 47
3.3.2 LiftingUnaryOperators . . . . . . . . . . . . . . . . . . . . . . 48
3.3.3Binary . . . . . . . . . . . . . . . . . . . . . . 49
3.3.4 MatrixMultiplication . . . . . . . . . . . . . . . . . . . . . . . 50
3.3.4.1 Distributivity . . . . . . . . . . . . . . . . . . . . . . . 51
3.3.4.2 Associativity . . . . . . . . . . . . . . . . . . . . . . . 51
3.3.5 Lattice OrderedRings . . . . . . . . . . . . . . . . . . . . . . . 51
3.3.6 PositivePartandNegativePart . . . . . . . . . . . . . . . . . . 53
3.4 ProvingBoundsbyDuality . . . . . . . . . . . . . . . . . . . . . . . . 54
3.5 PrInfeasibilitybyModifiedDuality . . . . . . . . . . . . . . . . 55
3.6 SparseMatrices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.7 IntervalArithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 574 Contents
3.7.1 Floats . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.7.2 DivisionofFloats . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.7.3 BasicIntervalArithmeticforFloats . . . . . . . . . . . . . . . . 60
3.7.4 ApproximationofMatrices . . . . . . . . . . . . . . . . . . . . 63
3.8 CalculatingAPrioriBounds . . . . . . . . . . . . . . . . . . . . . . . . 63
4 TheBasicLinearPrograms 65
4.1 TheArchiveOfTameGraphs . . . . . . . . . . . . . . . . . . . . . . . 65
4.2 GraphSystems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.2.1 TopologyofaGraphSystem . . . . . . . . . . . . . . . . . . . 68
4.2.2 3 SpaceInterpretationofaGraphSystem . . . . . . . . . . . . 69
4.2.3 AdditionalConstraintsofa . . . . . . . . . . . 72
4.3 GeneratingandRunningtheBasicLinearPrograms . . . . . . . . . . 73
A GraphSystemAxiomsfromtheInequalityDatabase 75
B ResultsofRunningtheBasicLPs 79
ListofFigures 87
Bibliography 89CHAPTER 1
Introduction
There are two conflicting primal impulses of
the human mind – one to simplify a thing to
its essentials, the other to see through the
essentials to the greater implications.
—RobertB.Laughlin
The Flyspeck project [14] has as its goal the complete formalization of Hales’
proof [15, 16] of the Kepler conjecture which states that the best density one can
hopeforwhenpackinginfinitelymanycongruentballsis
π
√ ≈0.74
18
Theformalizationhastobecarriedoutwithinamechanicaltheoremprover. For
our work described in this thesis, we have chosen the interactive proof assistant
Isabelle[25].
The proof of the Kepler conjecture proceeds in reducing the problem to a finite
number of possible counter examples, the tame graphs. In a previous research
effort[23],theenumerationofalltamegraphshasbeenformalizedandverified.
The final computational step of the Kepler conjecture is to prove by linear pro
gramming that all of these tame graphs cannot correspond to optimal packings,
exceptthosecorrespondingtotheface centeredcubicorhexagonal closepacking.
In this thesis we focus on the basic linear programs, which are an important first
milestoneoftakingthisfinalstep. Withtheirhelp,wecaneliminate2565ofthe2771
tamegraphs.
How reliable is this result? The major source of potential mayhem is that some
mistakemighthavebeenintroducedinthespecificationofthebasiclinearprograms.
Thecorrectnessofthisspecificationwillonlybeestablishedafterusingtheobtained
resultsinthelargercontextofacompleteformalproofoftheKeplerconjecture. But
evenifthereissuchanerror,wecanconsoleourselvesthatthemethodspresented
inthisthesisaregeneralenoughsothatatransfertoacorrectedspecificationshould
bepossible,andprobablyeasy.
Another potential source of mistakes is the use of the HOL Computing Library2 Chapter 1 — Introduction
which we introduce and describe in the next chapter. After all, it is just a piece of
unverifiedsoftwarewhichhasbeentestedbyonlyoneperson.
Apartfromthat,theusualclaimsofcomputer checkedproofshold.