ConeMappedWalk.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.walkKind_cycle line 24
lemma OAI.HyperbolicObstruction.ConeSkeleton.same_top_face line 29
def OAI.HyperbolicObstruction.ConeSkeleton.mappedMacroPolygon line 45
Source documentation
The actual simple macro polygon carried by one free source face. Its vertices are the original TEMPLATE vertices in their original cyclic order, not the possibly identified letter-bouquet vertices. This supplies the finite macro-cycle perimeter/three-fan bounds from the produced normal picture.
```
noncomputable def mappedMacroPolygon (hs : P.Simple) (hb : P.NoBigon)
    (x : P.Dart) (a : Top n w) (e : MacroGraph.graph.Dart) (hx : P.index x = .inl (a,e)) :
    MacroGraph.Polygon := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.MacroGraph.Polygon
lemma OAI.HyperbolicObstruction.ConeSkeleton.mappedMacroPolygon_size line 86

theorem OAI.HyperbolicObstruction.ConeSkeleton.normalizedMacroRows line 93

Source documentation

Source normal-form output now has all the actual macro cardinal bounds; no Polygon or perimeter field is assumed of the raw picture.

theorem normalizedMacroRows : ∃ Q : WalkPicture.{u} (walkTarget n w d c hc f),
    Nonempty (P.Retains Q) ∧ Q.Simple ∧ Q.NoBigon ∧ Q.Reduced ∧
      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.walkTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.mappedMacroPolygon