OAI/Combinatorics/StripMass/PairingDiagrams.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.IsPairing line 17
  2. abbrev OAI.CriticalStrip.Diagram.Pairing line 23
  3. instance OAI.CriticalStrip.Diagram.(instance at line 25) line 25
  4. instance OAI.CriticalStrip.Diagram.(instance at line 26) line 26
  5. def OAI.CriticalStrip.Diagram.empty line 28
  6. def OAI.CriticalStrip.Diagram.Pairing.Adj line 30
  7. def OAI.CriticalStrip.Diagram.Pairing.Occupied line 33
  8. theorem OAI.CriticalStrip.Diagram.empty_not_adj line 36
  9. theorem OAI.CriticalStrip.Diagram.empty_not_occupied line 38
  10. theorem OAI.CriticalStrip.Diagram.Pairing.adj_irrefl line 41
  11. theorem OAI.CriticalStrip.Diagram.Pairing.eq_empty_iff line 44
  12. inductive OAI.CriticalStrip.Diagram.Tile line 53
  13. instance OAI.CriticalStrip.Diagram.(instance at line 58) line 58
  14. def OAI.CriticalStrip.Diagram.Tile.edges line 62
  15. def OAI.CriticalStrip.Diagram.Tile.Adj line 73
  16. def OAI.CriticalStrip.Diagram.Tile.Occupied line 75
  17. theorem OAI.CriticalStrip.Diagram.Tile.vacant_not_adj line 77
  18. theorem OAI.CriticalStrip.Diagram.Tile.vacant_not_occupied line 79
  19. theorem OAI.CriticalStrip.Diagram.Tile.eq_vacant_iff line 82
  20. structure OAI.CriticalStrip.Diagram.Weights line 86
  21. def OAI.CriticalStrip.Diagram.Weights.tile line 93
  22. abbrev OAI.CriticalStrip.Diagram.Vertex line 101
  23. abbrev OAI.CriticalStrip.Diagram.Configuration line 102
  24. def OAI.CriticalStrip.Diagram.Wiring line 106
  25. def OAI.CriticalStrip.Diagram.Reach line 113
  26. structure OAI.CriticalStrip.Diagram.Realizes line 118
  27. def OAI.CriticalStrip.Diagram.column line 129
  28. def OAI.CriticalStrip.Diagram.identityWeights line 136
  29. def OAI.CriticalStrip.Diagram.deletionWeights line 137
  30. def OAI.CriticalStrip.Diagram.lambda line 139
  31. def OAI.CriticalStrip.Diagram.L line 140
  32. def OAI.CriticalStrip.Diagram.physicalWeights line 141
  33. def OAI.CriticalStrip.Diagram.transfer line 149
  34. abbrev OAI.CriticalStrip.Diagram.NonemptyPairing line 153
  35. def OAI.CriticalStrip.Diagram.restrictedColumn line 155
  36. def OAI.CriticalStrip.Diagram.VacuumRegular line 160
  37. theorem OAI.CriticalStrip.Diagram.realizes_empty_iff line 164
  38. theorem OAI.CriticalStrip.Diagram.column_empty_row line 194
  39. def OAI.CriticalStrip.Diagram.Pairing.map line 205
  40. def OAI.CriticalStrip.Diagram.Pairing.restrict line 228
  41. theorem OAI.CriticalStrip.Diagram.Pairing.restrict_adj line 247
  42. theorem OAI.CriticalStrip.Diagram.Pairing.map_adj_image line 254
  43. theorem OAI.CriticalStrip.Diagram.Pairing.restrict_map line 259
  44. def OAI.CriticalStrip.Diagram.Pairing.padBottom line 267
  45. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_adj_succ line 269
  46. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_not_adj_zero line 272
  47. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_not_adj_zero' line 277
  48. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_not_occupied_zero line 282
  49. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_occupied_succ line 286
  50. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_empty line 291
  51. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_eq_empty line 296
  52. theorem OAI.CriticalStrip.Diagram.Pairing.padBottom_restrict line 302
  53. def OAI.CriticalStrip.Diagram.Pairing.bottomVacantEquiv line 319
  54. def OAI.CriticalStrip.Diagram.Configuration.padBottom line 329
  55. theorem OAI.CriticalStrip.Diagram.Configuration.padBottom_zero line 331
  56. theorem OAI.CriticalStrip.Diagram.Configuration.padBottom_succ line 332
  57. def OAI.CriticalStrip.Diagram.vertexSucc line 337
  58. theorem OAI.CriticalStrip.Diagram.vertexSucc_injective line 339
  59. theorem OAI.CriticalStrip.Diagram.wiring_symm line 345
  60. theorem OAI.CriticalStrip.Diagram.reach_symm line 356
  61. theorem OAI.CriticalStrip.Diagram.wiring_padBottom_zero line 362
  62. theorem OAI.CriticalStrip.Diagram.wiring_padBottom_zero_right line 367
  63. theorem OAI.CriticalStrip.Diagram.wiring_padBottom_iff line 372
  64. theorem OAI.CriticalStrip.Diagram.reach_padBottom_image line 377
  65. theorem OAI.CriticalStrip.Diagram.reach_padBottom_iff line 390
  66. theorem OAI.CriticalStrip.Diagram.reach_padBottom_zero_iff line 400
  67. theorem OAI.CriticalStrip.Diagram.reach_padBottom_zero_right_iff line 405