LetterNormalPicture.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.ConeSkeleton.letterWordClosed line 15

theorem OAI.HyperbolicObstruction.ConeSkeleton.null_letter_word_normal_picture line 30

Source documentation

Diagram existence and normalization for the original letter presentation, not merely for a surrogate cone presentation. All literal outside positions survive. Every mixed interior face maps to an actual included source row, and no injectivity of random letter labels is assumed.

theorem null_letter_word_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