MacroRadialIndex.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.radialTemplate line 19
Source documentation
Read only the indexed radial port, not its numerical letter assignment, back into the subdivided macro template.
```
def radialTemplate : Dart n w → Option (MacroGraph.Vertex × MacroGraph.Vertex)
  | (.inl _,_) => none
  | (.inr ⟨b,v⟩,true) => some (MacroGraph.point b.val.1,
      match v.val with | .inl _ => .inr () | .inr l => .inl (.inr l))
  | (.inr _,false) => none
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.MacroGraph.Vertex, OAI.HyperbolicObstruction.MacroGraph.point
lemma OAI.HyperbolicObstruction.ConeSkeleton.macroStep_radialTemplate line 25
lemma OAI.HyperbolicObstruction.ConeSkeleton.macroStep_radial_injective line 41
lemma OAI.HyperbolicObstruction.ConeSkeleton.macroVertex_at_apex line 49