OAI/Geometry/HyperbolicGroups/GraphSquares.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.MasterGraph.code_injective line 15
2. lemma OAI.HyperbolicObstruction.MasterGraph.twoPath_complete line 27

   Source documentation

   Every literal nonbacktracking core two-path is one of the ninety square slots, up to reversal.

   lemma twoPath_complete {a b c : CoreGeometry.Vertex}
       (hab : CoreGeometry.Adjacent a b) (hbc : CoreGeometry.Adjacent b c) (hac : a ≠ c) :
       ∃ τ : TwoPath, (left τ = a ∧ middle τ = b ∧ right τ = c) ∨
         (left τ = c ∧ middle τ = b ∧ right τ = a) := by
   …

   Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex, OAI.HyperbolicObstruction.CoreGeometry.Adjacent, OAI.HyperbolicObstruction.MasterGraph.left, OAI.HyperbolicObstruction.MasterGraph.middle, OAI.HyperbolicObstruction.MasterGraph.right

3. lemma OAI.HyperbolicObstruction.MasterGraph.square_core_ne line 52
4. lemma OAI.HyperbolicObstruction.MasterGraph.admissible_square_pair line 58
5. lemma OAI.HyperbolicObstruction.MasterGraph.first_mem_square line 63
6. lemma OAI.HyperbolicObstruction.MasterGraph.second_mem_square line 65
7. lemma OAI.HyperbolicObstruction.MasterGraph.fresh_mem_square line 67