OAI/Geometry/HyperbolicGroups/ConeTopCollapse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.CoreWordGraph.label_congr line 13
2. lemma OAI.HyperbolicObstruction.CoreWordGraph.word_congr line 19
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.slot_radial_word line 34
4. def OAI.HyperbolicObstruction.ConeSkeleton.macroBase line 43
5. def OAI.HyperbolicObstruction.ConeSkeleton.macroRoute line 51

   Source documentation

   Send apex i to its fixed actual fan base and expand radial edges by fixed fan paths. The exceptional two-step incidence uses the genuine loose letter, not a fictitious eighth fan.

   def macroRoute {u v : MacroGraph.Vertex} (h : MacroGraph.Adjacent u v) :
       (CoreWordGraph.graph Finset.univ).Walk (macroBase u) (macroBase v) := by
   …

   Mentions: OAI.HyperbolicObstruction.MacroGraph.Vertex, OAI.HyperbolicObstruction.MacroGraph.Adjacent, OAI.HyperbolicObstruction.CoreWordGraph.graph, OAI.HyperbolicObstruction.ConeSkeleton.macroBase

6. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroRoute_length line 74
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroRoute_word line 97
8. def OAI.HyperbolicObstruction.ConeSkeleton.topCollapsedWalk line 120
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.topCollapsedWalk_length line 124
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.topCollapsedWalk_word line 130
11. theorem OAI.HyperbolicObstruction.ConeSkeleton.top_collapse_filling line 142

    Source documentation

    Every actual simple top polygon collapses to a core closed walk of length at most thirty, and hence to at most thirty exact finite-presentation faces.

    theorem top_collapse_filling (a : TopPolygon n w) :
        ∃ k ≤ 30, WordPictures.Homotopy (SimpleWordRelator n w d)
          (collapsedBoundary n w d (.inr (.inl a))) [] k := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.TopPolygon, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.collapsedBoundary