OAI/Combinatorics/StripMass/HalfTurn.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.Tile.turn line 17
  2. lemma OAI.CriticalStrip.Diagram.Tile.turn_turn line 24
  3. lemma OAI.CriticalStrip.Diagram.Tile.turn_vacant line 25
  4. lemma OAI.CriticalStrip.Diagram.Tile.turn_physical line 26
  5. lemma OAI.CriticalStrip.Diagram.Tile.turn_occupied_zero line 28
  6. lemma OAI.CriticalStrip.Diagram.Tile.turn_occupied_one line 30
  7. lemma OAI.CriticalStrip.Diagram.Tile.turn_occupied_two line 32
  8. lemma OAI.CriticalStrip.Diagram.Tile.turn_occupied_three line 34
  9. lemma OAI.CriticalStrip.Diagram.Tile.turn_middle line 36
  10. lemma OAI.CriticalStrip.Diagram.Tile.turn_weight line 37
  11. def OAI.CriticalStrip.turnTriangle line 44
  12. lemma OAI.CriticalStrip.turnTriangle_in_strip line 47
  13. lemma OAI.CriticalStrip.turnTriangle_turnTriangle line 50
  14. lemma OAI.CriticalStrip.turnTriangle_adjacent line 57
  15. lemma OAI.CriticalStrip.PathBetween.turn line 68
  16. def OAI.CriticalStrip.HoneycombAssignment.turn line 92
  17. lemma OAI.CriticalStrip.HoneycombAssignment.turn_tile line 111
  18. lemma OAI.CriticalStrip.HoneycombAssignment.turn_turn line 114
  19. lemma OAI.CriticalStrip.HoneycombAssignment.turn_up_adj line 123
  20. lemma OAI.CriticalStrip.HoneycombAssignment.turn_adj line 150
  21. lemma OAI.CriticalStrip.HoneycombAssignment.turn_edge line 171
  22. lemma OAI.CriticalStrip.HoneycombAssignment.turn_reach line 180
  23. lemma OAI.CriticalStrip.HoneycombAssignment.turn_drains line 185
  24. structure OAI.CriticalStrip.TopArchConfiguration line 198
  25. lemma OAI.CriticalStrip.TopArchConfiguration.ext line 206
  26. def OAI.CriticalStrip.TopArchConfiguration.toArch line 211
  27. def OAI.CriticalStrip.TopArchConfiguration.ofArch line 227
  28. lemma OAI.CriticalStrip.TopArchConfiguration.ofArch_toArch line 243
  29. lemma OAI.CriticalStrip.TopArchConfiguration.toArch_ofArch line 248
  30. def OAI.CriticalStrip.TopArchConfiguration.equivArch line 253
  31. theorem OAI.CriticalStrip.Diagram.PaddedColumn.runs_exists line 277
  32. lemma OAI.CriticalStrip.Diagram.PaddedColumn.runs_iff line 301
  33. def OAI.CriticalStrip.NorthExtension.tile line 326
  34. lemma OAI.CriticalStrip.NorthExtension.physical line 330
  35. lemma OAI.CriticalStrip.NorthExtension.south line 334
  36. lemma OAI.CriticalStrip.NorthExtension.west line 343
  37. lemma OAI.CriticalStrip.NorthExtension.east line 361
  38. lemma OAI.CriticalStrip.NorthExtension.north line 379
  39. lemma OAI.CriticalStrip.NorthExtension.middle line 383
  40. lemma OAI.CriticalStrip.NorthExtension.nonvacant line 397
  41. def OAI.CriticalStrip.TopArchConfiguration.extend line 408
  42. lemma OAI.CriticalStrip.TopArchConfiguration.extend_last line 432
  43. lemma OAI.CriticalStrip.TopArchConfiguration.extend_base line 435
  44. lemma OAI.CriticalStrip.TopArchConfiguration.extend_restrict line 439
  45. lemma OAI.CriticalStrip.TopArchConfiguration.extend_base_edge line 447
  46. lemma OAI.CriticalStrip.TopArchConfiguration.extend_up_edge line 455
  47. lemma OAI.CriticalStrip.TopArchConfiguration.extend_next_edge line 463
  48. lemma OAI.CriticalStrip.TopArchConfiguration.extend_up_reach line 471
  49. lemma OAI.CriticalStrip.TopArchConfiguration.extend_enter line 485
  50. lemma OAI.CriticalStrip.TopArchConfiguration.extend_drains_right line 493
  51. lemma OAI.CriticalStrip.TopArchConfiguration.extend_drains line 531