OAI/Combinatorics/StripMass/SewnAssignment.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_occupied_zero line 15
  2. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_occupied_one line 17
  3. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_occupied_two line 19
  4. lemma OAI.CriticalStrip.Diagram.Tile.horizontal_occupied_three line 21
  5. def OAI.CriticalStrip.SewnRectangle.tile line 30
  6. lemma OAI.CriticalStrip.SewnRectangle.tile_left line 36
  7. lemma OAI.CriticalStrip.SewnRectangle.tile_right line 41
  8. lemma OAI.CriticalStrip.SewnRectangle.tile_outside line 44
  9. lemma OAI.CriticalStrip.SewnRectangle.split_column line 47
  10. lemma OAI.CriticalStrip.SewnRectangle.physical line 53
  11. lemma OAI.CriticalStrip.SewnRectangle.horizontal line 64
  12. lemma OAI.CriticalStrip.SewnRectangle.vertical line 86
  13. def OAI.CriticalStrip.SewnRectangle.assignment line 99
  14. lemma OAI.CriticalStrip.SewnRectangle.south_vacant line 110
  15. lemma OAI.CriticalStrip.SewnRectangle.north_vacant line 119
  16. lemma OAI.CriticalStrip.SewnRectangle.physical_from_weights line 127
  17. lemma OAI.CriticalStrip.Diagram.Graph.drainsAt_iff line 167
  18. lemma OAI.CriticalStrip.Diagram.Graph.drainsAt_glued_iff line 176
  19. lemma OAI.CriticalStrip.Diagram.GraphRealizes.compressed_closure_edge line 192
  20. lemma OAI.CriticalStrip.Diagram.GraphRealizes.closure_compressed_edge line 201
  21. lemma OAI.CriticalStrip.Diagram.GraphRealizes.compressed_closure_reach line 209
  22. lemma OAI.CriticalStrip.Diagram.GraphRealizes.compressed_closure_drains line 222
  23. theorem OAI.CriticalStrip.Diagram.GraphRealizes.sewn_drains_iff line 236
  24. theorem OAI.CriticalStrip.Diagram.GraphRealizes.gluesAt_iff_sewn line 249
  25. abbrev OAI.CriticalStrip.Diagram.PaddedColumn.V line 266
  26. def OAI.CriticalStrip.Diagram.PaddedColumn.wiring line 268
  27. def OAI.CriticalStrip.Diagram.PaddedColumn.boundary line 274
  28. lemma OAI.CriticalStrip.Diagram.PaddedColumn.boundary_injective line 276
  29. def OAI.CriticalStrip.Diagram.PaddedColumn.active line 279
  30. lemma OAI.CriticalStrip.Diagram.PaddedColumn.wiring_nil line 282
  31. lemma OAI.CriticalStrip.Diagram.PaddedColumn.empty_realizes line 290
  32. def OAI.CriticalStrip.Diagram.PaddedColumn.addColumn line 307
  33. lemma OAI.CriticalStrip.Diagram.PaddedColumn.wiring_step line 317
  34. def OAI.CriticalStrip.Diagram.PaddedColumn.stepEquivalence line 349
  35. theorem OAI.CriticalStrip.Diagram.PaddedColumn.runs_realizes line 357
  36. lemma OAI.CriticalStrip.Diagram.Graph.drainsAt_embedding_iff line 389
  37. def OAI.CriticalStrip.SewnRectangle.port line 418
  38. lemma OAI.CriticalStrip.SewnRectangle.port_injective line 422
  39. lemma OAI.CriticalStrip.SewnRectangle.mem_range_port line 437
  40. lemma OAI.CriticalStrip.SewnRectangle.horizontalPort_eq line 444
  41. lemma OAI.CriticalStrip.SewnRectangle.wiring_left line 448
  42. lemma OAI.CriticalStrip.SewnRectangle.wiring_right line 473
  43. lemma OAI.CriticalStrip.SewnRectangle.wiring_cross line 510
  44. theorem OAI.CriticalStrip.SewnRectangle.sewn_wiring line 534
  45. lemma OAI.CriticalStrip.SewnRectangle.sewn_drains_iff line 564
  46. theorem OAI.CriticalStrip.SewnRectangle.gluesAt_physical_iff line 577