OAI/Geometry/HyperbolicGroups/ConeFullNormal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.ConeSkeleton.normalizedPicture line 29

   Source documentation

   Full actual mixed-cell normal form, with literal complete frozen face maps as the only raw indexing condition. Every finite genus-zero input is normalized by the checked surgeries, without assuming any fan link data, contact bound, or filling estimate.

   theorem normalizedPicture (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f)) :
       ∃ Q : WalkPicture.{u} (walkTarget n w d c hc f),
         Nonempty (P.Survives Q) ∧ Q.FrozenMapped (walkFrozenTarget n w d c hc f) ∧
         Q.Simple ∧ Q.NoBigon ∧ Q.FullyReduced ∧ Q.RadialInjective (isApex n w) ∧
         Q.chain = P.chain ∧
         ∀ (hs : Q.Simple) (hb : Q.NoBigon) (x : Q.Dart) (a : Top n w)
           (e : MacroGraph.graph.Dart) (hx : Q.index x = .inl (a,e)),
           Fintype.card {y : Q.Dart // Q.pairing.face.SameCycle x y} ≤ 15 ∧
             3 ≤ (mappedMacroPolygon n w d c hc f Q hs hb x a e hx).points.card := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.walkTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.mappedMacroPolygon