OAI/Geometry/HyperbolicGroups/MacroWalk.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.MacroGraph.graph line 14
2. def OAI.HyperbolicObstruction.MacroGraph.ofCycle line 20

   Source documentation

   The actual vertex-simple macro polygon obtained from a library cycle.

   def ofCycle {u : Vertex} (p : graph.Walk u u) (hp : p.IsCycle) : Polygon where
   …

   Mentions: OAI.HyperbolicObstruction.MacroGraph.Vertex, OAI.HyperbolicObstruction.MacroGraph.Polygon

3. theorem OAI.HyperbolicObstruction.MacroGraph.cycle_perimeter line 66
4. theorem OAI.HyperbolicObstruction.MacroGraph.cycle_points line 69
5. theorem OAI.HyperbolicObstruction.MacroGraph.normalize_walk line 76

   Source documentation

   Literal top-cone walks, including all repeats, have a finite simple-cycle normalization preserving any specified antisymmetric lifted triangle chain. No minimum diagram or abstract polygon hypothesis is used here.

   theorem normalize_walk {A : Type*} [AddCommGroup A]
       (c : graph.Dart → A) (hc : ∀ d, c d.symm = -c d)
       {u : Vertex} (p : graph.Walk u u) :
       ∃ cs : List (ConeWalks.Circuit graph),
         ConeWalks.chain c p = ConeWalks.total c cs ∧
         ConeWalks.perimeter cs ≤ p.length ∧
         ∀ q ∈ cs, q.2.val.length ≤ 15 ∧ 3 ≤ (ofCycle q.2.val q.2.property).points.card := by
   …

   Mentions: OAI.HyperbolicObstruction.MacroGraph.Vertex, OAI.HyperbolicObstruction.ConeWalks.Circuit, OAI.HyperbolicObstruction.MacroGraph.graph, OAI.HyperbolicObstruction.ConeWalks.chain, OAI.HyperbolicObstruction.ConeWalks.total, OAI.HyperbolicObstruction.ConeWalks.perimeter, OAI.HyperbolicObstruction.MacroGraph.ofCycle