OAI/Geometry/HyperbolicGroups/ConeDiskNormal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellToWalk_exterior_iff line 22
2. theorem OAI.HyperbolicObstruction.ConeSkeleton.nullWord_normal_picture line 59

   Source documentation

   Disk producer for the finite polygonal cone target: a nonempty closed literal nullword has a genus-zero mixed picture in the full normal form, with all outside positions and labels preserved. No existence of a disk diagram, normal form, or boundary matching is assumed.

   theorem nullWord_normal_picture
       (h : PresentedGroup.mk (FreeGroup.mk '' Set.range (boundary n w d).attachingWord)
         (FreeGroup.mk (List.ofFn word)) = 1) :
       ∃ (Q : WalkPicture.{0} (exteriorWalkTarget n w d ell hell word closed c hc f))
         (xs : List Q.Dart),
         Q.FrozenMapped (exteriorWalkFrozen n w d ell hell word closed 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 word closed c hc f).label ∘ Q.index) = List.ofFn word ∧
         (∀ x, (walkTarget n w d c hc f).isExterior ell hell word closed (Q.index x) ↔ x ∈ xs) ∧
         (∀ x s, Q.index x = .inr s → s.2.1 = true) := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkTarget, OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkFrozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.walkTarget