OAI/Geometry/HyperbolicGroups/MacroFaceFilling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.macro_parametrization_card line 20

   Source documentation

   The source's fifteen-side bound read directly from the actual cyclic macro-face parametrization, without identifying random letters.

   lemma macro_parametrization_card (p : Perm D) (j : D → MacroGraph.graph.Dart)
       (hc : ∀ x, (j (p x)).fst = (j x).snd)
       (hi : Function.Injective (fun x => (j x).fst))
       (hb : ∀ x, p (p x) ≠ x) : Fintype.card D ≤ 15 := by
   …

2. theorem OAI.HyperbolicObstruction.ConeSkeleton.macro_boundary_filling line 44

   Source documentation

   A literal bounded free macro face has a cost at most thirty in the exact finite simple-cycle presentation, via genuine core-graph routes.

   theorem macro_boundary_filling (a : Top n w) (p : Perm D) (j : D → MacroGraph.graph.Dart)
       (hc : ∀ x, (j (p x)).fst = (j x).snd)
       (hi : Function.Injective (fun x => (j x).fst))
       (hb : ∀ x, p (p x) ≠ x)
       (xs : List D) (hx : IsBoundary p xs) (hne : xs ≠ []) :
       ∃ k ≤ 30, WordPictures.Homotopy (SimpleWordRelator n w d)
         ((xs.map (fun x => macroStep n w a (j x).adj)).flatMap (collapse n w)) [] k := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.macroStep, OAI.HyperbolicObstruction.ConeSkeleton.collapse