1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Lemma: Main Linear Programs *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
12 This file contains definitions related to the main linear programming model.
21 let sol0 = new_definition `sol0 = &3 * acs (&1 / &3) - pi`;;
22 let rhom = new_definition `rhom y = &1 + sol0 / pi - lfun (y/ &2) * sol0/pi`;;
23 let rho218 = new_definition `rho218 = rhom (#2.18)`;;
24 let tgt_exact = new_definition `tgt_exact = &4 * pi - &20 * sol0`;;
26 (* The model has a hypermap (D,e,n,f) with
27 set of nodes V, edges E, faces F,
29 std_faces_not_super : set of faces.
30 super8 : set of faces.
31 superduperq : set of faces.
34 declare a type for decorated hypermaps.
37 Each standard fan gives a decorated hypermap.