OAI/Geometry/HyperbolicGroups/WalkNormal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.simple_front line 21
2. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.opposite_distinct_faces line 38
3. theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.normalize line 57

   Source documentation

   Top-walk surgery terminates on actual corner cardinality. It splits repeated template vertices, removes free backtracks and cancels a shared macro side of one occurrence even when the surrounding simple polygons are different. There is no assumed minimality or desired normal form here. All frozen faces and their individual side indices survive the surgery, and the exact signed elementary cone chain is unchanged.

   theorem normalize : ∃ Q : WalkPicture.{u} T,
       Nonempty (P.Retains Q) ∧ Q.Simple ∧ Q.NoBigon ∧ Q.Reduced ∧ Q.chain = P.chain := by
   …