WalkConeLink.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_apex_cases line 25
lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_top_adjacent_different line 64
Source documentation
Consecutive top turns in one normalized apex link cannot belong to the same top occurrence, even when their simple macro polygons are different.
```
lemma walk_top_adjacent_different (hred : P.FullyReduced) {x : P.Dart}
    {a b : Top n w} {e k : MacroGraph.graph.Dart}
    (hx : P.index x = .inl (a,e)) (hy : P.index (P.pairing.vertex x) = .inl (b,k))
    (ha : isApex n w (start n w (walkLabel n w d (P.index x))) = true) : a ≠ b := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.walkLabel
lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_top_unique_turn line 88
Source documentation
Two turns of one simple source top face over the same ACTUAL fan are identical. The argument retains the indexed fan type even if numerical letters and row fields repeat.
```
lemma walk_top_unique_turn (hs : P.Simple) {x y : P.Dart} {a : Top n w}
    {e : MacroGraph.graph.Dart} (hx : P.index x = .inl (a,e))
    (hxy : P.pairing.face.SameCycle x y) (b : Fan n w)
    (hax : start n w (walkLabel n w d (P.index x)) = .inr b)
    (hay : start n w (walkLabel n w d (P.index y)) = .inr b) : x = y := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.walkLabel
lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_apex_no_fixed line 107
lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_link_card line 117