OAI/Geometry/HyperbolicGroups/ConeGraph.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.CoreRow line 17
2. def OAI.HyperbolicObstruction.ConeSkeleton.extendCore line 19
3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Top line 25

   Source documentation

   Only the 32 actual top fields index a top occurrence. Decorations are NOT extra coordinates indexing redundant copies of a top cone.

   abbrev Top := {a : CoreRow n //
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.CoreRow

4. def OAI.HyperbolicObstruction.ConeSkeleton.slot line 29
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.slot_type line 32
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.top_row_injective line 34
7. def OAI.HyperbolicObstruction.ConeSkeleton.letterDart line 43
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.rev_rev line 45
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.rev_letter line 48
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.start_letter line 51
11. def OAI.HyperbolicObstruction.ConeSkeleton.macroVertex line 54
12. def OAI.HyperbolicObstruction.ConeSkeleton.loose line 58
13. def OAI.HyperbolicObstruction.ConeSkeleton.macroStep line 62

    Source documentation

    The literal map of the subdivided incidence graph from source02:72--79. The exceptional two-edge path is radial X_D followed by the loose letter.

    def macroStep (a : Top n w) {u v : MacroGraph.Vertex} (h : MacroGraph.Adjacent u v) : Dart n w := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.MacroGraph.Vertex, OAI.HyperbolicObstruction.MacroGraph.Adjacent, OAI.HyperbolicObstruction.ConeSkeleton.Dart

14. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroStep_start line 78
15. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroStep_reverse line 91
16. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroStep_end line 104
17. abbrev OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle line 111

    Source documentation

    Each fan triangle retains its original edge field and BOTH distinct radial ports, independently of repetitions in the assigned generator row.

    abbrev FanTriangle := Σ b : Fan n w, {e : IncidenceTemplate.Edge // e ∈ fan b.val.1}

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.IncidenceTemplate.Edge

18. def OAI.HyperbolicObstruction.ConeSkeleton.fanLetter line 113
19. def OAI.HyperbolicObstruction.ConeSkeleton.fanLeft line 116
20. def OAI.HyperbolicObstruction.ConeSkeleton.fanRight line 118
21. def OAI.HyperbolicObstruction.ConeSkeleton.fanSide line 121
22. lemma OAI.HyperbolicObstruction.ConeSkeleton.fanSide_closed line 125