OAI/Combinatorics/StripMass/PairingSurgery.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.IsPairing.mono line 16
  2. theorem OAI.CriticalStrip.Diagram.Pairing.adj_symm line 23
  3. theorem OAI.CriticalStrip.Diagram.Pairing.adj_unique line 26
  4. def OAI.CriticalStrip.Diagram.Pairing.Cross line 43
  5. theorem OAI.CriticalStrip.Diagram.Pairing.not_cross line 49
  6. def OAI.CriticalStrip.Diagram.Pairing.omitTwo line 62
  7. theorem OAI.CriticalStrip.Diagram.Pairing.omitTwo_adj line 66
  8. theorem OAI.CriticalStrip.Diagram.Pairing.not_cross_iff_between line 72
  9. theorem OAI.CriticalStrip.Diagram.Pairing.cap_no_cross line 80
  10. def OAI.CriticalStrip.Diagram.Pairing.orderedEdge line 91
  11. theorem OAI.CriticalStrip.Diagram.Pairing.orderedEdge_lt line 93
  12. theorem OAI.CriticalStrip.Diagram.Pairing.occupied_of_mem line 98
  13. theorem OAI.CriticalStrip.Diagram.Pairing.cap_new_edge_disjoint line 102
  14. def OAI.CriticalStrip.Diagram.Pairing.capSplice line 120
  15. def OAI.CriticalStrip.Diagram.Pairing.mapOccupied line 170
  16. theorem OAI.CriticalStrip.Diagram.Pairing.mapOccupied_adj line 198
  17. theorem OAI.CriticalStrip.Diagram.Pairing.swap_adjacent_order line 203
  18. def OAI.CriticalStrip.Diagram.Pairing.moveIntoVacancy line 210
  19. theorem OAI.CriticalStrip.Diagram.Pairing.swap_adjacent_order_lower line 217
  20. def OAI.CriticalStrip.Diagram.Pairing.moveIntoLowerVacancy line 223
  21. def OAI.CriticalStrip.Diagram.Pairing.insertCup line 229
  22. def OAI.CriticalStrip.Diagram.Pairing.partner line 265
  23. theorem OAI.CriticalStrip.Diagram.Pairing.partner_adj line 268
  24. theorem OAI.CriticalStrip.Diagram.Pairing.adjacent_partners line 271
  25. theorem OAI.CriticalStrip.Diagram.Pairing.capSplice_adj line 283
  26. theorem OAI.CriticalStrip.Diagram.Pairing.capSplice_occupied line 292
  27. theorem OAI.CriticalStrip.Diagram.Pairing.omitTwo_not_occupied_left line 308
  28. theorem OAI.CriticalStrip.Diagram.Pairing.omitTwo_not_occupied_right line 311
  29. def OAI.CriticalStrip.Diagram.Pairing.capRemove line 316
  30. theorem OAI.CriticalStrip.Diagram.Pairing.capRemove_vacant line 322
  31. def OAI.CriticalStrip.Diagram.Pairing.tileStep line 333