(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma:  Main Linear Programs                                                      *)
(* Chapter:                                                                *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-06-14                                                           *)
(* ========================================================================== *)


(*
This file contains definitions related to the main linear programming model.
*)

(*
changes
delta0 -> sol0

*)

let sol0 = new_definition `sol0 = &3 * acs (&1 / &3)  - pi`;;
let rhom = new_definition `rhom y = &1 + sol0 / pi - lfun (y/ &2) * sol0/pi`;;
let rho218 = new_definition `rho218 = rhom (#2.18)`;;
let tgt_exact = new_definition `tgt_exact = &4 * pi - &20 * sol0`;;

(* The model has a hypermap (D,e,n,f) with 
    set of nodes V, edges E, faces F,

   std_faces_not_super : set of faces.
   super8 : set of faces.
   superduperq : set of faces.
   ....

   declare a type for decorated hypermaps.


   Each standard fan gives a decorated hypermap.

 *)