OAI/GroupTheory/ArtinCAT0/Folding.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArtinCAT0.TriangleMesh.foldPartner line 9
  2. structure OAI.ArtinCAT0.TriangleMesh.Fold line 13
  3. def OAI.ArtinCAT0.TriangleMesh.Fold.Removed line 24
  4. abbrev OAI.ArtinCAT0.TriangleMesh.Fold.Kept line 25
  5. abbrev OAI.ArtinCAT0.TriangleMesh.Fold.partner line 26
  6. lemma OAI.ArtinCAT0.TriangleMesh.Fold.partner_f line 28
  7. lemma OAI.ArtinCAT0.TriangleMesh.Fold.partner_g line 30
  8. lemma OAI.ArtinCAT0.TriangleMesh.Fold.partner_outside line 33
  9. lemma OAI.ArtinCAT0.TriangleMesh.Fold.partner_partner line 37
  10. lemma OAI.ArtinCAT0.TriangleMesh.Fold.partner_removed line 51
  11. lemma OAI.ArtinCAT0.TriangleMesh.Fold.partner_ne line 57
  12. lemma OAI.ArtinCAT0.TriangleMesh.Fold.mate_seam_reverse line 65
  13. lemma OAI.ArtinCAT0.TriangleMesh.Fold.mate_partner_outside line 68
  14. def OAI.ArtinCAT0.TriangleMesh.Fold.splice line 78
  15. lemma OAI.ArtinCAT0.TriangleMesh.Fold.splice_inside line 82
  16. lemma OAI.ArtinCAT0.TriangleMesh.Fold.splice_outside line 84
  17. lemma OAI.ArtinCAT0.TriangleMesh.Fold.splice_kept line 87
  18. lemma OAI.ArtinCAT0.TriangleMesh.Fold.splice_splice line 94
  19. lemma OAI.ArtinCAT0.TriangleMesh.Fold.splice_ne line 103
  20. def OAI.ArtinCAT0.TriangleMesh.Fold.merge line 113
  21. lemma OAI.ArtinCAT0.TriangleMesh.Fold.merge_opposite line 117
  22. lemma OAI.ArtinCAT0.TriangleMesh.Fold.tail_seam line 121
  23. lemma OAI.ArtinCAT0.TriangleMesh.Fold.tail_seam_reverse line 125
  24. lemma OAI.ArtinCAT0.TriangleMesh.Fold.merge_tail_partner line 129
  25. abbrev OAI.ArtinCAT0.TriangleMesh.Fold.oldDart line 142
  26. lemma OAI.ArtinCAT0.TriangleMesh.Fold.oldDart_kept line 144
  27. def OAI.ArtinCAT0.TriangleMesh.Fold.newMate line 147
  28. lemma OAI.ArtinCAT0.TriangleMesh.Fold.oldDart_newMate line 151
  29. lemma OAI.ArtinCAT0.TriangleMesh.Fold.oldDart_injective line 154
  30. lemma OAI.ArtinCAT0.TriangleMesh.Fold.newMate_involutive line 160
  31. def OAI.ArtinCAT0.TriangleMesh.Fold.mesh line 165
  32. def OAI.ArtinCAT0.TriangleMesh.Fold.toNewDart line 181
  33. lemma OAI.ArtinCAT0.TriangleMesh.Fold.oldDart_toNewDart line 184
  34. lemma OAI.ArtinCAT0.TriangleMesh.Fold.toNewDart_oldDart line 187
  35. def OAI.ArtinCAT0.TriangleMesh.Fold.sideValue line 190
  36. lemma OAI.ArtinCAT0.TriangleMesh.Fold.sideValue_partner line 194
  37. def OAI.ArtinCAT0.TriangleMesh.Fold.extension line 211
  38. lemma OAI.ArtinCAT0.TriangleMesh.Fold.extension_outside line 217
  39. lemma OAI.ArtinCAT0.TriangleMesh.Fold.extension_f_zero line 223
  40. lemma OAI.ArtinCAT0.TriangleMesh.Fold.extension_g_zero line 227
  41. lemma OAI.ArtinCAT0.TriangleMesh.Fold.extension_removed_nonzero line 231
  42. lemma OAI.ArtinCAT0.TriangleMesh.Fold.extension_mate line 235
  43. lemma OAI.ArtinCAT0.TriangleMesh.Fold.sideValue_g_one line 274
  44. lemma OAI.ArtinCAT0.TriangleMesh.Fold.sideValue_g_two line 279
  45. lemma OAI.ArtinCAT0.TriangleMesh.Fold.extension_face line 284
  46. theorem OAI.ArtinCAT0.TriangleMesh.Fold.mesh_exact line 306

    Source documentation

    Deleting the opposite pair preserves exactness of edge cocycles.

    theorem mesh_exact (he : M.Exact) : C.mesh.Exact := by
…
  47. def OAI.ArtinCAT0.TriangleMesh.active line 337
  48. lemma OAI.ArtinCAT0.TriangleMesh.active_exact line 344
  49. lemma OAI.ArtinCAT0.TriangleMesh.active_surjective line 349
  50. def OAI.ArtinCAT0.TriangleMesh.phaseEquiv line 353
  51. lemma OAI.ArtinCAT0.TriangleMesh.phaseEquiv_apply line 359
  52. lemma OAI.ArtinCAT0.TriangleMesh.phaseEquiv_symm_apply line 361
  53. lemma OAI.ArtinCAT0.TriangleMesh.phaseEquiv_rotate line 364
  54. def OAI.ArtinCAT0.TriangleMesh.rephase line 368
  55. lemma OAI.ArtinCAT0.TriangleMesh.rephase_exact line 384
  56. def OAI.ArtinCAT0.xLetter line 410
  57. def OAI.ArtinCAT0.hLetter line 414
  58. def OAI.ArtinCAT0.positiveDirection line 416
  59. def OAI.ArtinCAT0.negativeDirection line 417
  60. def OAI.ArtinCAT0.reverseDirection line 418
  61. lemma OAI.ArtinCAT0.reverseDirection_reverseDirection line 420
  62. def OAI.ArtinCAT0.cellDirection line 427

    Source documentation

    Directed sides, retaining the literal nine labels, not just their group values.

    def cellDirection (b i s t : Fin 3) : LinkDirection :=
…

    Mentions: OAI.ArtinCAT0.LinkDirection

  63. lemma OAI.ArtinCAT0.cellDirection_reverse line 435
  64. abbrev OAI.ArtinCAT0.CornerOrder line 438
  65. def OAI.ArtinCAT0.cellFlag line 440
  66. lemma OAI.ArtinCAT0.cellFlag_injective line 443
  67. lemma OAI.ArtinCAT0.cellFlag_adjacent line 446
  68. lemma OAI.ArtinCAT0.cellDirection_injective line 449
  69. def OAI.ArtinCAT0.cornerSign line 454

    Source documentation

    Orientation sign of the vertex correspondence.

    def cornerSign (p : CornerOrder) : ℤ := if p 1 = p 0 + 1 then 1 else -1

    Mentions: OAI.ArtinCAT0.CornerOrder

  70. def OAI.ArtinCAT0.reverseCorner line 456
  71. lemma OAI.ArtinCAT0.cornerSign_reverse line 458
  72. structure OAI.ArtinCAT0.TargetTriangle line 461
  73. def OAI.ArtinCAT0.TargetTriangle.vertex line 466
  74. def OAI.ArtinCAT0.TargetTriangle.direction line 469
  75. lemma OAI.ArtinCAT0.TargetTriangle.vertex_injective line 472
  76. structure OAI.ArtinCAT0.TriangleMesh.Labeling line 490

    Source documentation

    Complete cell identities and vertex correspondences; compatibility includes labelled directions rather than merely equal group elements.

    structure Labeling where
…
  77. def OAI.ArtinCAT0.TriangleMesh.Labeling.direction line 503
  78. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.direction_mate line 506
  79. def OAI.ArtinCAT0.TriangleMesh.Labeling.cornerShift line 509
  80. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.cornerShift_apply line 515
  81. def OAI.ArtinCAT0.TriangleMesh.Labeling.cornerAt line 517
  82. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.direction_turn line 519
  83. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.flag_cornerAt line 533
  84. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.link_adjacent line 539
  85. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.mate_face_ne line 545
  86. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.cellFlag_reverse line 554
  87. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.backtrack_cell line 558
  88. def OAI.ArtinCAT0.TriangleMesh.Labeling.active line 588
  89. def OAI.ArtinCAT0.TriangleMesh.Labeling.rephase line 595
  90. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.orders_of_seam line 609
  91. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.order_seam_remaining line 622
  92. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.order_seam_sign line 625
  93. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.order_seam_mate line 628
  94. def OAI.ArtinCAT0.TriangleMesh.Labeling.seamFold line 633
  95. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.vertex_merge line 669
  96. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.direction_partner line 679
  97. def OAI.ArtinCAT0.TriangleMesh.Labeling.folded line 694
  98. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.exists_equal_mates line 708
  99. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.exists_phased_seam line 717
  100. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.cornerSign_shift line 736
  101. def OAI.ArtinCAT0.TriangleMesh.Labeling.signedSum line 739
  102. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.signedSum_active line 742
  103. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.signedSum_rephase line 745
  104. lemma OAI.ArtinCAT0.TriangleMesh.Labeling.signedSum_folded line 749
  105. theorem OAI.ArtinCAT0.TriangleMesh.signed_counts_zero line 773

    Source documentation

    Every exact finite labelled triangular mesh has zero algebraic count on each individual target triangle. No manifold or embedding theorem is assumed.

    theorem signed_counts_zero (w : TargetTriangle → ℤ) :
    ∀ (F : Type u) (V : Type v) [Fintype F] (M : TriangleMesh F V) (L : M.Labeling),
      M.Exact → L.signedSum w = 0 := by
…

    Mentions: OAI.ArtinCAT0.TargetTriangle, OAI.ArtinCAT0.TriangleMesh