OAI/GroupTheory/Hyperbolic/LiftedFilling.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release075.BlockPresentation.edgeValue line 11

    Source documentation

    The signed displacement of an oriented original edge, with the two tree edges already killed in the actual presentation.

    def edgeValue (e : d.OrientedEdge) : d.GroupType :=
…
  2. theorem OAI.Release075.BlockPresentation.edgeValue_flip line 14
  3. def OAI.Release075.BlockPresentation.wordValue line 19
  4. theorem OAI.Release075.BlockPresentation.wordValue_nil line 21
  5. theorem OAI.Release075.BlockPresentation.wordValue_cons line 22
  6. theorem OAI.Release075.BlockPresentation.wordValue_append line 24
  7. abbrev OAI.Release075.BlockPresentation.LiftedEdge line 28
  8. abbrev OAI.Release075.BlockPresentation.LiftedVertex line 29
  9. def OAI.Release075.BlockPresentation.liftedFlip line 31
  10. def OAI.Release075.BlockPresentation.liftedTarget line 34
  11. theorem OAI.Release075.BlockPresentation.liftedFlip_flip line 36
  12. theorem OAI.Release075.BlockPresentation.liftedTarget_ne line 41
  13. def OAI.Release075.BlockPresentation.LiftedFace line 48

    Source documentation

    A genuine lift of a triangular face: all three corners are glued at the same group coordinates, not merely at the same original vertex colors.

    def LiftedFace (a b c : d.LiftedEdge) : Prop :=
…
  14. theorem OAI.Release075.BlockPresentation.LiftedFace.rotate line 54
  15. theorem OAI.Release075.BlockPresentation.LiftedFace.mirror line 57
  16. theorem OAI.Release075.BlockPresentation.LiftedFace.colors line 64
  17. theorem OAI.Release075.BlockPresentation.LiftedFace.unique line 71
  18. def OAI.Release075.BlockPresentation.liftWord line 77
  19. theorem OAI.Release075.BlockPresentation.liftWord_nil line 81
  20. theorem OAI.Release075.BlockPresentation.liftWord_cons line 82
  21. theorem OAI.Release075.BlockPresentation.liftWord_length line 85
  22. theorem OAI.Release075.BlockPresentation.liftWord_forget line 91
  23. theorem OAI.Release075.BlockPresentation.liftWord_append line 97
  24. theorem OAI.Release075.BlockPresentation.liftWord_typed line 104
  25. theorem OAI.Release075.BlockPresentation.TriangleFace.value line 115
  26. theorem OAI.Release075.BlockPresentation.TriangleFace.lift line 125
  27. theorem OAI.Release075.BlockPresentation.rawMove_wordValue line 139
  28. theorem OAI.Release075.BlockPresentation.rawHomotopic_wordValue line 153
  29. theorem OAI.Release075.BlockPresentation.rawMove_lifted_filled line 164
  30. theorem OAI.Release075.BlockPresentation.rawHomotopic_lifted_filled line 197
  31. theorem OAI.Release075.BlockPresentation.nullhomotopic_lifted_fillable line 228
  32. def OAI.Release075.TriangleFilling.forgetLift line 243

    Source documentation

    Forgetting group coordinates keeps every dart, incidence, boundary and planar component. The metric labels can therefore be tracked through reduction.

    def forgetLift (D : TriangleFilling d.liftedFlip d.liftedTarget d.LiftedFace w) :
    TriangleFilling d.flipEdge d.edgeTarget d.TriangleFace (w.map Prod.fst) where
…

    Mentions: OAI.Release075.TriangleFilling

  33. theorem OAI.Release075.TriangleFilling.forgetLift_activeCount line 260
  34. def OAI.Release075.TriangleFilling.Dipole.lift line 266

    Source documentation

    Matching opposite face labels at a shared lifted edge forces matching group coordinates on the other two edges. Thus reduction cannot hide a downstairs dipole.

    def Dipole.lift {D : TriangleFilling d.liftedFlip d.liftedTarget d.LiftedFace w}
    (P : D.forgetLift.Dipole) : D.Dipole := by
…

    Mentions: OAI.Release075.TriangleFilling

  35. theorem OAI.Release075.TriangleFilling.noDipole_forgetLift line 302
  36. theorem OAI.Release075.MarkedLineData.exists_lifted_linear_filling line 311