OAI/Geometry/HyperbolicGroups/PolygonDiskProducer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.outsideTarget line 23
2. theorem OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.nullWord_picture line 30

   Source documentation

   Every nonempty literal null word produces an actual mapped genus-zero cell picture with ONE distinguished exterior boundary. Every other face maps with its own indexed enumeration to a genuine attaching polygon, in either orientation. The exterior has positive orientation and coefficient zero.

   theorem nullWord_picture (hinv : B.rev = invLetter)
       (h : PresentedGroup.mk (FreeGroup.mk '' Set.range B.attachingWord)
         (FreeGroup.mk (List.ofFn word)) = 1) :
       ∃ (Q : CellPicture.{0} (B.outsideTarget ell hell word closed weight apex radial))
         (xs : List Q.Dart), IsBoundary Q.pairing.face xs ∧
         xs.map ((B.outsideTarget ell hell word closed weight apex radial).edge ∘ Q.index) = List.ofFn word ∧
         ∀ x, B.outsideTag ell hell word closed (Q.index x) =
           if x ∈ xs then some true else none := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.weight, OAI.HyperbolicObstruction.PictureSwitch.IsBoundary