OAI/Geometry/HyperbolicGroups/WordPictureFilling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.filling line 19

   Source documentation

   Actual planar side pairings produce area-counted word homotopies. This uses genus zero essentially (the one-face leaf), not an unproved diagram realization axiom. Both finite incidence and face counts bound the cost.

   theorem filling {w : Word A} (P : WordPicture R w) :
       ∃ n, Homotopy R w [] n ∧ n ≤ Fintype.card P.Dart / 2 ∧
         (n : ℤ) ≤ cycles P.pairing.face := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.WordPicture, OAI.HyperbolicObstruction.WordPictures.Homotopy