OAI/Geometry/HyperbolicGroups/ElementaryCone.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroCell_representative line 15
2. def OAI.HyperbolicObstruction.ConeSkeleton.macroCellDart line 35

   Source documentation

   A canonical positive orientation, with exactly ONE elementary triangle per unoriented macro edge. No redundant simple-cycle disks are introduced.

   def macroCellDart (c : MacroCell) : MacroGraph.graph.Dart := (macroCell_representative c).choose

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.MacroCell, OAI.HyperbolicObstruction.ConeSkeleton.macroCell_representative

3. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroCellDart_cell line 36
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.macroCellDart_orientation line 38
5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryVertex line 47

   Source documentation

   The actual pre-compression finite incidence data: old fan apices, separate top apices, every labelled radial edge, and elementary triangles. This data is not claimed to be a constructed topological CW space.

   abbrev ElementaryVertex := Vertex n w ⊕ Top n w

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Vertex, OAI.HyperbolicObstruction.ConeSkeleton.Top

6. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryEdge line 48
7. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart line 49
8. abbrev OAI.HyperbolicObstruction.ConeSkeleton.ElementaryCell line 50
9. def OAI.HyperbolicObstruction.ConeSkeleton.elementaryOld line 52
10. def OAI.HyperbolicObstruction.ConeSkeleton.elementaryRev line 53
11. def OAI.HyperbolicObstruction.ConeSkeleton.elementaryStart line 54
12. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryRev_rev line 59
13. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOld_rev line 63
14. def OAI.HyperbolicObstruction.ConeSkeleton.elementaryTriangle line 68

    Source documentation

    The three literal sides of a top cone triangle, including its two new radial edges; arbitrary repeated OLD endpoints remain allowed.

    def elementaryTriangle (a : Top n w) (e : MacroGraph.graph.Dart) : Fin 3 → ElementaryDart n w :=
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart

15. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryTriangle_closed line 71
16. def OAI.HyperbolicObstruction.ConeSkeleton.elementarySize line 81
17. def OAI.HyperbolicObstruction.ConeSkeleton.elementarySide line 85
18. def OAI.HyperbolicObstruction.ConeSkeleton.elementaryBoundary line 90

    Source documentation

    Full boundary certificate for the actual elementary two-cells.

    def elementaryBoundary : PolygonTarget.Boundary (ElementaryCell n w d) (ElementaryDart n w)
        (ElementaryVertex n w) where
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryCell, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryVertex

19. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryCell_eq_chain_index line 105

    Source documentation

    The elementary cells have the SAME independent lift indices as the integral chain endpoint, not the redundant auxiliary polygon-cell indices.

    lemma elementaryCell_eq_chain_index :
        ElementaryCell n w d = ((Top n w × MacroCell) ⊕ FrozenCell n w d) := rfl
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryCell, OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.MacroCell, OAI.HyperbolicObstruction.ConeSkeleton.FrozenCell

20. def OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage line 115

    Source documentation

    Extension to the actual top radial edges. Deck coordinates of a top lift are measured at its apex, so all of its elementary triangles have the same apex coordinate used by LiftedCellularChain.

    def elementaryVoltage : ElementaryDart n w → G
      | (.inl e,b) => v (e,b)
      | (.inr a,true) => macroPotential n w v a.1 a.2
      | (.inr a,false) => (macroPotential n w v a.1 a.2)⁻¹
    
    include hv in

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart, OAI.HyperbolicObstruction.ConeSkeleton.macroPotential

21. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage_rev line 121
22. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage_triangle line 128
23. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage_cell line 136
24. lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterVoltage_cell line 143

    Source documentation

    Unconditional original-group values on the actual pre-compression cells.

    lemma elementaryLetterVoltage_cell (a : ElementaryCell n w d) :
        (List.ofFn (fun i => elementaryVoltage n w (letterVoltage n w d)
          (elementarySide n w d a i))).prod = 1 :=
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryCell, OAI.HyperbolicObstruction.ConeSkeleton.elementaryVoltage, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage, OAI.HyperbolicObstruction.ConeSkeleton.elementarySide