OAI/Geometry/HyperbolicGroups/ConeWalkTarget.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.FrozenCell line 20

    Source documentation

    Actual non-top cells; these faces must not be split during macro surgery.

    abbrev FrozenCell := FanTriangle n w ⊕ (Square n w ⊕ Six n d)

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.Square, OAI.HyperbolicObstruction.ConeSkeleton.Six

  2. def OAI.HyperbolicObstruction.ConeSkeleton.frozenCell line 22
  3. def OAI.HyperbolicObstruction.ConeSkeleton.frozenBoundary line 26
  4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.WalkStep line 35
  5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.WalkKind line 36
  6. abbrev OAI.HyperbolicObstruction.ConeSkeleton.WalkVertex line 37
  7. def OAI.HyperbolicObstruction.ConeSkeleton.walkKind line 39
  8. def OAI.HyperbolicObstruction.ConeSkeleton.walkFree line 43
  9. def OAI.HyperbolicObstruction.ConeSkeleton.walkFront line 47
  10. def OAI.HyperbolicObstruction.ConeSkeleton.walkBack line 51
  11. def OAI.HyperbolicObstruction.ConeSkeleton.walkVertex line 55
  12. def OAI.HyperbolicObstruction.ConeSkeleton.walkLabel line 59
  13. def OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite line 63
  14. lemma OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite_kind line 67
  15. lemma OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite_label line 71
  16. lemma OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite_front line 77
  17. lemma OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite_back line 85
  18. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_loopless line 95
  19. lemma OAI.HyperbolicObstruction.ConeSkeleton.walk_simple line 102
  20. def OAI.HyperbolicObstruction.ConeSkeleton.walkWeight line 122

    Source documentation

    A frozen oriented face contributes its cellular coefficient once, at its zero-th POSITION, not once per side. Top steps contribute their individually indexed oriented elementary cone triangles.

    def walkWeight (c : Top n w → MacroGraph.graph.Dart → A) (f : FrozenCell n w d → A) :
    WalkStep n w d → A
  | .inl s => c s.1 s.2
  | .inr s => if s.2.2.val = 0 then (frozenBoundary n w d).weight f s else 0

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.FrozenCell, OAI.HyperbolicObstruction.ConeSkeleton.WalkStep, OAI.HyperbolicObstruction.ConeSkeleton.frozenBoundary

  21. lemma OAI.HyperbolicObstruction.ConeSkeleton.walkWeight_opposite line 127
  22. def OAI.HyperbolicObstruction.ConeSkeleton.walkTarget line 140

    Source documentation

    Literal target for the actual top occurrences and their subdivided macro edges. No simple-cycle or normal-picture assertion is included in this data. In particular two DISTINCT top polygons using a common indexed cone side are recognized as cancellable.

    def walkTarget (c : Top n w → MacroGraph.graph.Dart → A)
    (hc : ∀ a e, c a e.symm = -c a e) (f : FrozenCell n w d → A) :
    WalkCellTarget (WalkStep n w d) (WalkKind n w d) (WalkVertex n w)
      (Dart n w) (Vertex n w) A where
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.FrozenCell, OAI.HyperbolicObstruction.ConeSkeleton.WalkStep, OAI.HyperbolicObstruction.ConeSkeleton.WalkKind, OAI.HyperbolicObstruction.ConeSkeleton.WalkVertex, OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.ConeSkeleton.Vertex