OAI/Geometry/HyperbolicGroups/GraphWordFilling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.GraphWordFilling.word line 16
2. lemma OAI.HyperbolicObstruction.GraphWordFilling.word_nil line 17
3. lemma OAI.HyperbolicObstruction.GraphWordFilling.word_cons line 18
4. lemma OAI.HyperbolicObstruction.GraphWordFilling.word_append line 20
5. lemma OAI.HyperbolicObstruction.GraphWordFilling.word_length line 23
6. lemma OAI.HyperbolicObstruction.GraphWordFilling.short_filling line 26
7. theorem OAI.HyperbolicObstruction.GraphWordFilling.path_filling line 49

   Source documentation

   Quantitative noncommutative loop erasure. Each deleted elementary cycle costs one, and each backtrack costs zero. The residual path pays for its own length; no relator injection or distinct-letter assumption is needed.

   theorem path_filling (r : G.Dart → A × Bool)
       (hr : ∀ e, r e.symm = ((r e).1,!(r e).2)) (R : Set (Word A))
       (hR : ∀ (u : V) (p : G.Walk u u), p.IsCycle → word r p ∈ R)
       {u v : V} (p : G.Walk u v) :
       ∃ (q : G.Walk u v) (a : ℕ), q.IsPath ∧
         Homotopy R (word r p) (word r q) a ∧ a + q.length ≤ p.length := by
   …

   Mentions: OAI.HyperbolicObstruction.GraphWordFilling.word

8. theorem OAI.HyperbolicObstruction.GraphWordFilling.closed_filling line 90

   Source documentation

   A closed graph walk of length L has a disk derivation over its simple cycles using at most L relator disks.

   theorem closed_filling (r : G.Dart → A × Bool)
       (hr : ∀ e, r e.symm = ((r e).1,!(r e).2)) (R : Set (Word A))
       (hR : ∀ (u : V) (p : G.Walk u u), p.IsCycle → word r p ∈ R)
       {u : V} (p : G.Walk u u) :
       ∃ a ≤ p.length, Homotopy R (word r p) [] a := by
   …

   Mentions: OAI.HyperbolicObstruction.GraphWordFilling.word