OAI/Geometry/HyperbolicGroups/GraphLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.MasterGraph.array line 31

   Source documentation

   The actual graph-valued orbit array, uniformly bounded using the fixed finite route to each vertex.

   def array (v : Vertex) : OrbitLimit.Array (Ω := Ω) O where
   …

   Mentions: OAI.HyperbolicObstruction.MasterGraph.Vertex, OAI.HyperbolicObstruction.OrbitLimit.Array

2. abbrev OAI.HyperbolicObstruction.MasterGraph.limit line 43
3. lemma OAI.HyperbolicObstruction.MasterGraph.side line 47
4. lemma OAI.HyperbolicObstruction.MasterGraph.path_lower line 60
5. lemma OAI.HyperbolicObstruction.MasterGraph.square_twoStep line 74
6. theorem OAI.HyperbolicObstruction.MasterGraph.metricCore line 109

   Source documentation

   Source Proposition configuration (i), constructed from matches, paths, unit edge expectations, and decorating-square rigidity.

   theorem metricCore : CoreGeometry.MetricCore
       (fun v => limit (U := U) O A letter hact g hM (.inl v)) := by
   …

   Mentions: OAI.HyperbolicObstruction.CoreGeometry.MetricCore, OAI.HyperbolicObstruction.MasterGraph.limit