OAI/Combinatorics/Hamiltonian/PairPhases.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Paired states, permutation cycle classes, and phase cancellation.

  1. def OAI.Barnette.phase line 9
  2. theorem OAI.Barnette.phase_add_six line 11
  3. theorem OAI.Barnette.phase_sub_six line 17
  4. theorem OAI.Barnette.disk_count_identity line 22
  5. def OAI.Barnette.TriangleSystem.rawIndexSum line 30
  6. instance OAI.Barnette.TriangleSystem.(instance at line 33) line 33
  7. def OAI.Barnette.TriangleSystem.OppositeCycle.faceSet line 40
  8. theorem OAI.Barnette.TriangleSystem.OppositeCycle.mem_faceSet line 44
  9. def OAI.Barnette.TriangleSystem.OppositeCycle.cyclicDelta line 48
  10. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reverse_rawIndexSum_diff line 51
  11. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reverse_phase line 81
  12. theorem OAI.Barnette.TriangleSystem.OppositeCycle.fixed_second_state_cancels line 91
  13. def OAI.Barnette.CycleClass line 115
  14. def OAI.Barnette.classOf line 117
  15. instance OAI.Barnette.(instance at line 119) line 119
  16. theorem OAI.Barnette.classOf_apply line 122
  17. theorem OAI.Barnette.classOf_symm_apply line 126
  18. theorem OAI.Barnette.classOf_surjective line 131
  19. theorem OAI.Barnette.classOf_eq_iff line 134
  20. theorem OAI.Barnette.invariant_on_cycle line 137
  21. def OAI.Barnette.descendCycle line 149
  22. theorem OAI.Barnette.descendCycle_classOf line 153
  23. def OAI.Barnette.partialPerm line 156
  24. theorem OAI.Barnette.partialPerm_apply line 165
  25. def OAI.Barnette.TriangleSystem.State.ofPermutation line 175
  26. def OAI.Barnette.TriangleSystem.Pair line 189
  27. def OAI.Barnette.TriangleSystem.Pair.left line 193
  28. def OAI.Barnette.TriangleSystem.Pair.right line 194
  29. theorem OAI.Barnette.TriangleSystem.Pair.partner line 196
  30. theorem OAI.Barnette.TriangleSystem.Pair.ext line 198
  31. instance OAI.Barnette.TriangleSystem.Pair.(instance at line 201) line 201
  32. instance OAI.Barnette.TriangleSystem.Pair.(instance at line 202) line 202
  33. def OAI.Barnette.TriangleSystem.Pair.next line 204
  34. theorem OAI.Barnette.TriangleSystem.Pair.value_next line 207
  35. theorem OAI.Barnette.TriangleSystem.Pair.value_prev line 212
  36. theorem OAI.Barnette.TriangleSystem.Pair.next_ne line 217
  37. def OAI.Barnette.TriangleSystem.Pair.third line 221
  38. def OAI.Barnette.TriangleSystem.Pair.Group line 224
  39. instance OAI.Barnette.TriangleSystem.Pair.(instance at line 226) line 226
  40. def OAI.Barnette.TriangleSystem.Pair.flipCorners line 229
  41. def OAI.Barnette.TriangleSystem.Pair.flipLeft line 232
  42. def OAI.Barnette.TriangleSystem.Pair.flipRight line 241
  43. theorem OAI.Barnette.TriangleSystem.Pair.flipLeft_val line 252
  44. theorem OAI.Barnette.TriangleSystem.Pair.flipRight_val line 256
  45. theorem OAI.Barnette.TriangleSystem.Pair.flipLeft_value line 260
  46. theorem OAI.Barnette.TriangleSystem.Pair.flipRight_value line 265
  47. def OAI.Barnette.TriangleSystem.Pair.flip line 270
  48. theorem OAI.Barnette.TriangleSystem.Pair.flip_third line 280
  49. def OAI.Barnette.TriangleSystem.Pair.orient line 286
  50. theorem OAI.Barnette.TriangleSystem.Pair.same_third_corners line 290
  51. theorem OAI.Barnette.TriangleSystem.Pair.group_local line 293
  52. def OAI.Barnette.TriangleSystem.Pair.bits line 301
  53. theorem OAI.Barnette.TriangleSystem.Pair.group_values line 304
  54. theorem OAI.Barnette.TriangleSystem.Pair.bits_invariant line 312
  55. def OAI.Barnette.TriangleSystem.Pair.orientations line 326
  56. theorem OAI.Barnette.TriangleSystem.Pair.orient_orientations line 329
  57. theorem OAI.Barnette.TriangleSystem.Pair.orientations_orient line 348
  58. def OAI.Barnette.TriangleSystem.Pair.groupEquiv line 359