OAI/Geometry/HyperbolicGroups/LetterFillingArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.ConeSkeleton.null_letter_word_counted_normal_picture line 22

   Source documentation

   Connected quantitative output for the original null word: a genuine protected normal disk AND a simple-relator filling bounded by thirty times its actual interior face count. No linear bound on that face count is assumed.

   theorem null_letter_word_counted_normal_picture
       (h : PresentedGroup.mk (Relator n w d) (FreeGroup.mk (List.ofFn word)) = 1) :
       ∃ (Q : WalkPicture.{0} (exteriorWalkTarget n w d ell hell (letterDart n w ∘ word)
           (letterWordClosed n w ell word) c hc f)) (xs : List Q.Dart),
         Q.FrozenMapped (exteriorWalkFrozen n w d ell hell (letterDart n w ∘ word)
           (letterWordClosed n w ell word) c hc f) ∧
         Q.Simple ∧ Q.NoBigon ∧ Q.FullyReduced ∧ Q.RadialInjective (isApex n w) ∧
         IsBoundary Q.pairing.face xs ∧
         xs.map ((exteriorWalkTarget n w d ell hell (letterDart n w ∘ word)
           (letterWordClosed n w ell word) c hc f).label ∘ Q.index) =
           List.ofFn (letterDart n w ∘ word) ∧
         (∀ x, (walkTarget n w d c hc f).isExterior ell hell (letterDart n w ∘ word)
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkTarget, OAI.HyperbolicObstruction.ConeSkeleton.letterDart, OAI.HyperbolicObstruction.ConeSkeleton.letterWordClosed, OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkFrozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.walkTarget