(* Notes on the hypermap chapter. new type: hypermap infixes: POWER, belong, iso. key definitions: orbit_map f x (the orbit of x under f), edge x (edge map orbit of x), node x, face x. edge_map, face_map, node_map (the permutations) *) (* Notes by Tom Hales in a conversation with TNT on Sep 9, 2010. TNT has completed essentially everything up the section with title "transform" The main theorem in the "transform" section is called AQIUNPP (markup transform). It is a long proof that is complete except for (flag1) and (flag2). TNT promises to send the completed proof of AQIUNPP on Sep 12, 2010. TNT's general naming convention is lemmaABC for the lemma with guid ABC. In particular, lemmaZHQCZLX; lemmaFKSNTKR; lemmaHOZKXVW; lemmaTGJISOK; lemmaIUCLZYI; lemmaBISHKQW; lemmaFOAGLPA; lemmaSGCOSXK; lemmaQZTPGJV; lemmaKDAEDEX; lemmaLIPYTUI; lemmaILTXRQD; lemmaICJHAOQ; lemmaJMKRXLA; lemmaHQYMRTX; lemmaQRDYXYJ. [Note: 2/15/2012 *On HYQMRTX, the furthermore clause in the flypaper hasn't been included in lemmaHQYMRTX. *I can't find lemmaQRDYXY. It must not have been uploaded. *Also found lemmaSTKBEPH. This is the algorithm termination; once there are sufficiently many loops in a normal family, it must be the collection of faces. This seems to have been deleted from flypaper.pdf. ] RDW. Reverse double walkup. This is not implemented as of Sep 2010. He plans to do it in two cases. The special case that does not add any new nodes and the general case. HLT needs the special case in the fans chapter. *) (* KHGAQRG. Not done as a separate lemma, but instead it appears many times as a subgoal. If you have a restricted hypermap and and f step, then you get a singleton. compare set_one_point, lemma_singleton_atom, . YBGABWW. Equivalent but not identical to theorems in TNT. PKRQTKP. There are many orbit theorems in hypermap.hl ZJIOZB (def of merge and split), ZMFKZNH (merge-split). Both TNT and Gonthier reverse things so that the lemma serves as a definition and the def is proved as a lemma. ZMFKZNH breaks into several formal lemmas: lemma_face_merge, lemma_edge_merge, lemma_node_merge. IUCLZYI. This has been formalized, but it is not used directly elsewhere. Instead, a number of smaller preliminary lemmas get used. EUXPBPO = lemmaThreeDarts // WIRLCNL. Something equivalent gets done in lemma_cycle_is_face and lemmaQuotientFace. UDJNSHH. Not formalized. Instead the proofs that rely on it go back to definitions instead. KSRDPTZ = lemmaQuotientNoDoubleJoints // PYOVATA = lemmaNodalFixedPoint (not exactly the same, the hypotheses are different) Note May 2012. QQYVCFM. Not formalized. dih2k defined in such a way to avoid lemma. WRGCVDR_CIZMRRH.hl defines dih2k in terms of the properties of QQYVCHEM. So it appears that QQYVCFM is not needed. cyclic_hypermap.hl and related notions are dead code, never used. KHGAQRG. Not formalized because TNT never needs to use it. *) (* Notes by Hales Feb 12, 2012. There are over 600 lemmas in the file. TNT has 108 definitions in his file, which makes it hard to understand the statements and how they related to the flypaper. Here is an informal summary of definitions. infixes: POWER, belong, iso Types: (A)hypermap with extraction functions dart (H:(A)hypermap -> edge_map node_map face_map edge H x ; edge orbit of dart x node H x ; node orbit of dart x face H x ; face orbit of dart x (A)loop with extraction functions. A loop is an unordered set (of darts) together with a permutation that acts transitively on he set. (This is what gets called torsor in flypaper.pdf.) dart_of ; dart set of loop next ; successor function back ; inverse of successor function belong ; in dart set size ; card of dart set top ; PRE(CARD dart_of L) is_loop H L ; x IN L ==>one_step_contour H x (next L x) loop_path L x k ; ((next L) POWER k) x; path out of loop starting at x. index L x y ; (specification) smallest i such that y = next^i x. Informal definitions: POWER : nth iterate of a function. orbit_map (f:A->A) (x:A) orbit of x under f go_one_step H x y <=> y is the image of dart x under e,n, or f. is_path H (p:num->A) (n:num) ; (p 0) ... (p n) is a dart path in H. is_in_component H x y ; darts x and y are in the same path component of H comb_component H x ; (same as is_in_component H x) set_of_orbits D f = set of orbits in D of f number_of_orbits D f = card of set_of_orbits edge_set H = set_of_orbits (dart H) (edge_map H) node_set H = set_of_orbits (dart H) (node_map H) face_set H = set_of_orbits (dart H) (face_map H) set_components H D = set of combinatorial components of all darts x in D set_part_components H D = same as set_components H D set_of_components H = set_components H (dart H) number_of_edges H = Klar number_of_nodes H = Klar number_of_faces H = Klar number_of_components H = Klar connected_hypermpa H = Klar plain_hypermap H planar_hypermap H simple_hypermap H is_no_double_joins H dart_degenerate H x; the dart x is fixed by e,n, or f. dart_nondegenerate H x; negation is_edge_nondegenerate is_node_nondegenerate is_face_nondegenerate isolated_dart ; x = f x = n x = e x. is_edge_degenerate ; x = e x but x != n x, x != f x. is_node_degenerate is_face_degenerae *** ** lists as functions p:num->A: ** : is_inj_list (p:num->A) n ; (p is 1-1 on 0..n) support_list (p:num->A) n ; { p i | i <= n} in_list p n ; i IN (support_list p n) is_disjoint p q glue p q n ; list concatenation. is_glueing p q n m ; This states roughly that no member of (q,m) is in (p,n), except (p n = q 0). Used to concatenate injective lists (p,n) @ (q,m). join p q n ; list concatenation, swallowing head of q. edge_path H x i = ((edge_map H) POWER i) x node_path H x i = similar face_path H x i = similar samsara p n x = the successor to x in list (p,n), wrapping to the beginning if necessary. *** contours one_step_contour H x y ; y = f x or n^{-1} x is_contour H p n ; (p,n) is a contour path node_contour H x i ; ((inverse (node_map H)) POWER i) x face_contour H x i ; ((face_map H) POWER i) x is_inj_contour H p n ; (p,n) is an injective contour path *** walkup shift H ; rotates (e,n,f) -> (n,f,e) triality of H. edge_walkup H x ; new hypermap after edge_walkup of H at x. node_walkup H x face_walkup H x double_edge_walkup H x y double_node_walkup H x y double_face_walkup H x y *** more on orbits power_list f x = \i. (f POWER i) x inj_orbit f x n ; the power_list of f x is an inj list (p,n) order_permutation ; the order of a permutation of finite order. *** merge is_edge_merge H x. is_node_merge is_face_merge is_edge_split is_node_split is_face_split is_splitting_component H x ; n x and e^{-1} x are in the same comb component of (edge_walkup H x) is_Moebius_contour H p k ; (p,k) is an (injective) Moebius contour shift_path p i ; \j. p (j + i) *** complements ind H x n ; mirror H x k n ; complement H x n =mirror H x n n ; implements complementary loop of face contour *** misc res (f:A->A) s ; restriction of function f to s, extension by identity. planar_ind H ; planar index iota iso H H' ; isomorphism of hypermap *** cyclic hypermap cyclic_hypermap ; darts two sets of k, cyc_emap, cyc_nmap, cyc_fmap. cyc_emap cyc_nmap cyc_fmap face map on cyclic hypermap *** quotients is_node_going H L x y ; n^{-1} steps from dart x to y in loop L atom H L x = the "atom" [ .... x;n^{-1} x ....] of x in loop L is_normal H NF ; NF is a normal family of loops. quotient_darts H NF ; set of atoms from loops in NF. support_darts NF ; darts visiting NF fmap ; face map on atoms emap ; edge map on atoms nmap ; node map on atoms quotient H NF ; quotient hypermap by a normal family NF. cycle H L ; set of atoms of L support_node H NF a ; set of darts of H at the node containing the atom a choice H NF x ; the atom containing x in the normal family. head H NF x; head of atom containing dart x. tail ; tail of a atom containing dart x face_loop H x ; returns the loop on the face of x. face_collection H ; the set of face loops. canon_loop H NF ; this says that every atom in NF has size 1. canon H NF ; the set of loops that are canonical canon_darts ; the set of darts of loops that are canonical canon_flag H NF ; this is not quite the way it is presented in flypaper. flag H NF L x ; *** m,p,q,x,y,z: minside H L x ; specification m st. next^i x = f^i x. mAdd H L x ; specification p st. f^{p+1} in support of NF. mRoute H L x ; specification q st ... dart_inside H NF L x. { f^i x | 1<= i <= m} heading H NF L x ; I think this is the dart y = f^{m+1} x. attach H NF L x ; I think this is the dart z = f^{p+1} y. *** restricted hypermaps is_restricted H is_split_condition H NF L x ; long list of hypotheses; needed to split a loop into two is_marked H NF L x; defines marked hypermap *** transform of hypermap genex H NF L x; glues "attach" dart to "heading" dart tpx H NF L x; I think this is the size of the new face? geney NF L x; glues "heading" dart to "attach" dart tpy H NF L x; again size of new face? dnax H NF L x ; new loop X dnay H NF L x = new loop Y genesis H NF L x = new set of loops, deleting L, adding two new loops. *)