ConeCellWalk.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.topDart line 15
Source documentation
The actual oriented macro edge in the indexed attaching polygon.
```
def topDart (a : TopPolygon n w) (i : Fin a.2.2.val.length) : MacroGraph.graph.Dart :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.TopPolygon
def OAI.HyperbolicObstruction.ConeSkeleton.cellWalkStep line 22
Source documentation
Forget only the choice of simple circuit surrounding a top step. Frozen fan/decorative cell identities and all their positions are retained.
```
def cellWalkStep : (boundary n w d).Side → WalkStep n w d
  | ⟨.inl a,b,i⟩ => .inr ⟨.inl a,b,i⟩
  | ⟨.inr (.inl a),b,i⟩ => .inl (a.1,if b then topDart n w a i else (topDart n w a i).symm)
  | ⟨.inr (.inr a),b,i⟩ => .inr ⟨.inr a,b,i⟩
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.WalkStep, OAI.HyperbolicObstruction.ConeSkeleton.topDart
lemma OAI.HyperbolicObstruction.ConeSkeleton.cellWalkStep_label line 27
lemma OAI.HyperbolicObstruction.ConeSkeleton.cellWalkStep_kind line 37
lemma OAI.HyperbolicObstruction.ConeSkeleton.cellWalkStep_closed line 43
lemma OAI.HyperbolicObstruction.ConeSkeleton.cellWalkStep_frozen_next line 59
lemma OAI.HyperbolicObstruction.ConeSkeleton.cellWalkStep_frozen_inj line 70
def OAI.HyperbolicObstruction.ConeSkeleton.cellToWalk line 107
Source documentation
Raw mixed pictures are now produced from actual indexed cellular pictures; no simple/reduced/fan-link condition is assumed at this bridge.
```
def cellToWalk : WalkPicture.{u} (walkTarget n w d c hc f) where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkTarget
lemma OAI.HyperbolicObstruction.ConeSkeleton.cellToWalk_frozen line 129