2 Notes on the hypermap chapter.
6 infixes: POWER, belong, iso.
8 key definitions: orbit_map f x (the orbit of x under f),
9 edge x (edge map orbit of x), node x, face x.
10 edge_map, face_map, node_map (the permutations)
18 Notes by Tom Hales in a conversation with TNT on Sep 9, 2010.
20 TNT has completed essentially everything up the section with title "transform"
21 The main theorem in the "transform" section is called AQIUNPP (markup transform).
22 It is a long proof that is complete except for (flag1) and (flag2). TNT promises
23 to send the completed proof of AQIUNPP on Sep 12, 2010.
25 TNT's general naming convention is lemmaABC for the lemma with guid
27 lemmaZHQCZLX; lemmaFKSNTKR; lemmaHOZKXVW; lemmaTGJISOK; lemmaIUCLZYI;
28 lemmaBISHKQW; lemmaFOAGLPA; lemmaSGCOSXK; lemmaQZTPGJV; lemmaKDAEDEX;
29 lemmaLIPYTUI; lemmaILTXRQD; lemmaICJHAOQ; lemmaJMKRXLA;
30 lemmaHQYMRTX; lemmaQRDYXYJ.
33 *On HYQMRTX, the furthermore clause in the flypaper hasn't been included in lemmaHQYMRTX.
34 *I can't find lemmaQRDYXY. It must not have been uploaded.
35 *Also found lemmaSTKBEPH. This is the algorithm termination; once there are sufficiently many
36 loops in a normal family, it must be the collection of faces. This seems to have been deleted
41 RDW. Reverse double walkup. This is not implemented as of Sep 2010.
42 He plans to do it in two cases. The special case that does not add
43 any new nodes and the general case. HLT needs the special case in
50 KHGAQRG. Not done as a separate lemma, but instead it appears many
51 times as a subgoal. If you have a restricted hypermap and and f step,
52 then you get a singleton. compare set_one_point,
53 lemma_singleton_atom, .
55 YBGABWW. Equivalent but not identical to theorems in TNT.
57 PKRQTKP. There are many orbit theorems in hypermap.hl
59 ZJIOZB (def of merge and split), ZMFKZNH (merge-split). Both TNT
60 and Gonthier reverse things so that the lemma serves as a definition
61 and the def is proved as a lemma.
63 ZMFKZNH breaks into several formal lemmas: lemma_face_merge,
64 lemma_edge_merge, lemma_node_merge.
66 IUCLZYI. This has been formalized, but it is not used directly
67 elsewhere. Instead, a number of smaller preliminary lemmas get
70 EUXPBPO = lemmaThreeDarts //
72 WIRLCNL. Something equivalent gets done in lemma_cycle_is_face and
75 UDJNSHH. Not formalized. Instead the proofs that rely on it go back
76 to definitions instead.
78 KSRDPTZ = lemmaQuotientNoDoubleJoints //
80 PYOVATA = lemmaNodalFixedPoint (not exactly the same, the hypotheses
84 QQYVCFM. Not formalized. dih2k defined in such a way to avoid lemma.
85 WRGCVDR_CIZMRRH.hl defines dih2k in terms of the properties
86 of QQYVCHEM. So it appears that QQYVCFM is not needed.
87 cyclic_hypermap.hl and related notions are dead code, never used.
89 KHGAQRG. Not formalized because TNT never needs to use it.
93 (* Notes by Hales Feb 12, 2012.
95 There are over 600 lemmas in the file.
97 TNT has 108 definitions in his file, which makes it hard to
98 understand the statements and how they related to the
99 flypaper. Here is an informal summary of definitions.
101 infixes: POWER, belong, iso
104 (A)hypermap with extraction functions
105 dart (H:(A)hypermap ->
110 edge H x ; edge orbit of dart x
111 node H x ; node orbit of dart x
112 face H x ; face orbit of dart x
114 (A)loop with extraction functions. A loop is an unordered set (of darts) together with a permutation
115 that acts transitively on he set. (This is what gets called torsor in flypaper.pdf.)
116 dart_of ; dart set of loop
117 next ; successor function
118 back ; inverse of successor function
120 size ; card of dart set
121 top ; PRE(CARD dart_of L)
122 is_loop H L ; x IN L ==>one_step_contour H x (next L x)
123 loop_path L x k ; ((next L) POWER k) x; path out of loop starting at x.
124 index L x y ; (specification) smallest i such that y = next^i x.
126 Informal definitions:
127 POWER : nth iterate of a function.
128 orbit_map (f:A->A) (x:A) orbit of x under f
129 go_one_step H x y <=> y is the image of dart x under e,n, or f.
130 is_path H (p:num->A) (n:num) ; (p 0) ... (p n) is a dart path in H.
131 is_in_component H x y ; darts x and y are in the same path component of H
132 comb_component H x ; (same as is_in_component H x)
133 set_of_orbits D f = set of orbits in D of f
134 number_of_orbits D f = card of set_of_orbits
136 edge_set H = set_of_orbits (dart H) (edge_map H)
137 node_set H = set_of_orbits (dart H) (node_map H)
138 face_set H = set_of_orbits (dart H) (face_map H)
139 set_components H D = set of combinatorial components of all darts x in D
140 set_part_components H D = same as set_components H D
141 set_of_components H = set_components H (dart H)
143 number_of_edges H = Klar
144 number_of_nodes H = Klar
145 number_of_faces H = Klar
146 number_of_components H = Klar
147 connected_hypermpa H = Klar
154 dart_degenerate H x; the dart x is fixed by e,n, or f.
155 dart_nondegenerate H x; negation
156 is_edge_nondegenerate
157 is_node_nondegenerate
158 is_face_nondegenerate
159 isolated_dart ; x = f x = n x = e x.
160 is_edge_degenerate ; x = e x but x != n x, x != f x.
165 ** lists as functions p:num->A: ** :
167 is_inj_list (p:num->A) n ; (p is 1-1 on 0..n)
168 support_list (p:num->A) n ; { p i | i <= n}
169 in_list p n ; i IN (support_list p n)
171 glue p q n ; list concatenation.
172 is_glueing p q n m ; This states roughly that no member of (q,m) is in (p,n), except (p n = q 0).
173 Used to concatenate injective lists (p,n) @ (q,m).
174 join p q n ; list concatenation, swallowing head of q.
176 edge_path H x i = ((edge_map H) POWER i) x
177 node_path H x i = similar
178 face_path H x i = similar
180 samsara p n x = the successor to x in list (p,n), wrapping to the beginning if necessary.
184 one_step_contour H x y ; y = f x or n^{-1} x
185 is_contour H p n ; (p,n) is a contour path
186 node_contour H x i ; ((inverse (node_map H)) POWER i) x
187 face_contour H x i ; ((face_map H) POWER i) x
188 is_inj_contour H p n ; (p,n) is an injective contour path
193 shift H ; rotates (e,n,f) -> (n,f,e) triality of H.
194 edge_walkup H x ; new hypermap after edge_walkup of H at x.
197 double_edge_walkup H x y
198 double_node_walkup H x y
199 double_face_walkup H x y
203 power_list f x = \i. (f POWER i) x
204 inj_orbit f x n ; the power_list of f x is an inj list (p,n)
206 order_permutation ; the order of a permutation of finite order.
217 is_splitting_component H x ; n x and e^{-1} x are in the same comb component of (edge_walkup H x)
218 is_Moebius_contour H p k ; (p,k) is an (injective) Moebius contour
220 shift_path p i ; \j. p (j + i)
226 complement H x n =mirror H x n n ; implements complementary loop of face contour
230 res (f:A->A) s ; restriction of function f to s, extension by identity.
232 planar_ind H ; planar index iota
234 iso H H' ; isomorphism of hypermap
238 cyclic_hypermap ; darts two sets of k, cyc_emap, cyc_nmap, cyc_fmap.
242 cyc_fmap face map on cyclic hypermap
247 is_node_going H L x y ; n^{-1} steps from dart x to y in loop L
248 atom H L x = the "atom" [ .... x;n^{-1} x ....] of x in loop L
249 is_normal H NF ; NF is a normal family of loops.
250 quotient_darts H NF ; set of atoms from loops in NF.
251 support_darts NF ; darts visiting NF
252 fmap ; face map on atoms
253 emap ; edge map on atoms
254 nmap ; node map on atoms
255 quotient H NF ; quotient hypermap by a normal family NF.
256 cycle H L ; set of atoms of L
257 support_node H NF a ; set of darts of H at the node containing the atom a
259 choice H NF x ; the atom containing x in the normal family.
260 head H NF x; head of atom containing dart x.
261 tail ; tail of a atom containing dart x
264 face_loop H x ; returns the loop on the face of x.
265 face_collection H ; the set of face loops.
267 canon_loop H NF ; this says that every atom in NF has size 1.
268 canon H NF ; the set of loops that are canonical
269 canon_darts ; the set of darts of loops that are canonical
271 canon_flag H NF ; this is not quite the way it is presented in flypaper.
276 minside H L x ; specification m st. next^i x = f^i x.
277 mAdd H L x ; specification p st. f^{p+1} in support of NF.
278 mRoute H L x ; specification q st ...
280 dart_inside H NF L x. { f^i x | 1<= i <= m}
281 heading H NF L x ; I think this is the dart y = f^{m+1} x.
282 attach H NF L x ; I think this is the dart z = f^{p+1} y.
284 *** restricted hypermaps
288 is_split_condition H NF L x ; long list of hypotheses; needed to split a loop into two
290 is_marked H NF L x; defines marked hypermap
292 *** transform of hypermap
294 genex H NF L x; glues "attach" dart to "heading" dart
295 tpx H NF L x; I think this is the size of the new face?
296 geney NF L x; glues "heading" dart to "attach" dart
297 tpy H NF L x; again size of new face?
298 dnax H NF L x ; new loop X
299 dnay H NF L x = new loop Y
301 genesis H NF L x = new set of loops, deleting L, adding two new loops.