OAI/Geometry/HyperbolicGroups/FaceWalk.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.FaceClosed line 22

   Source documentation

   A literal closed target walk on each source face: the next side starts where this side ends. This imposes no injectivity or normal form.

   def FaceClosed (M : PictureMap D) (source target : D → V) : Prop :=
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.FaceKind line 27

   Source documentation

   The indexed target occurrence stays constant around each source face. Distinct occurrence indices remain distinct even if their labels agree.

   def FaceKind (M : PictureMap D) (kind : D → C) : Prop := ∀ x, kind (M.face x) = kind x
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.kind_cycle line 30
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_closed line 35
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_kind line 43
6. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.normalize_simple_faces line 54

   Source documentation

   Split repeated vertex visits in selected kinds of closed polygon walks. Only face permutations change; all oriented steps, occurrence indices, edge pairings and therefore every additive cone-step chain are retained literally. Unselected faces retain their entire cyclic parametrization. The normalization is a finite maximization, not an assumed simple-polygon representative.

   theorem normalize_simple_faces (M : PictureMap D) (hG : M.GenusZero)
       (source target : D → V) (hc : M.FaceClosed source target)
       (kind : D → C) (hk : M.FaceKind kind) (free : C → Bool) :
       ∃ N : PictureMap D,
         N.edge = M.edge ∧ N.GenusZero ∧ N.FaceClosed source target ∧ N.FaceKind kind ∧
         (∀ x, free (kind x) = false → N.face x = M.face x) ∧
         ∀ a b, free (kind a) = true → N.face.SameCycle a b → target a = target b → a = b := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap