OAI/Combinatorics/StripMass/ColumnSew.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.BareColumn line 15
  2. def OAI.CriticalStrip.Diagram.ColumnSew.graph line 23
  3. def OAI.CriticalStrip.Diagram.ColumnSew.project line 26
  4. lemma OAI.CriticalStrip.Diagram.ColumnSew.bare_sub line 30
  5. lemma OAI.CriticalStrip.Diagram.ColumnSew.west line 36
  6. lemma OAI.CriticalStrip.Diagram.ColumnSew.west' line 39
  7. lemma OAI.CriticalStrip.Diagram.ColumnSew.project_edge line 42
  8. lemma OAI.CriticalStrip.Diagram.ColumnSew.include_edge line 54
  9. lemma OAI.CriticalStrip.Diagram.ColumnSew.old_used line 65
  10. lemma OAI.CriticalStrip.Diagram.ColumnSew.wiring_west_used line 71
  11. lemma OAI.CriticalStrip.Diagram.ColumnSew.project_used line 76
  12. lemma OAI.CriticalStrip.Diagram.ColumnSew.include_used line 86
  13. def OAI.CriticalStrip.Diagram.ColumnSew.equivalence line 99
  14. structure OAI.CriticalStrip.Diagram.ColumnCompatible line 119
  15. lemma OAI.CriticalStrip.Diagram.realizes_iff_column_graph line 125
  16. lemma OAI.CriticalStrip.Diagram.realizes_unique line 143
  17. lemma OAI.CriticalStrip.Diagram.realizes_exists_of_drains line 150
  18. def OAI.CriticalStrip.Diagram.ColumnChain.Vertices line 187
  19. def OAI.CriticalStrip.Diagram.ColumnChain.boundary line 191
  20. def OAI.CriticalStrip.Diagram.ColumnChain.support line 195
  21. def OAI.CriticalStrip.Diagram.ColumnChain.wiring line 199
  22. def OAI.CriticalStrip.Diagram.ColumnChain.Compatible line 204
  23. def OAI.CriticalStrip.Diagram.ColumnChain.Runs line 208
  24. lemma OAI.CriticalStrip.Diagram.ColumnChain.runs_sound line 212
  25. lemma OAI.CriticalStrip.Diagram.ColumnChain.runs_unique line 232
  26. lemma OAI.CriticalStrip.Diagram.ColumnChain.runs_exists line 236
  27. lemma OAI.CriticalStrip.Diagram.ColumnChain.runs_iff line 257
  28. abbrev OAI.CriticalStrip.Diagram.ColumnRectangle.V line 280
  29. def OAI.CriticalStrip.Diagram.ColumnRectangle.wiring line 284
  30. def OAI.CriticalStrip.Diagram.ColumnRectangle.boundary line 293
  31. def OAI.CriticalStrip.Diagram.ColumnRectangle.active line 297
  32. def OAI.CriticalStrip.Diagram.ColumnRectangle.addColumn line 302
  33. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.addColumn_old line 317
  34. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.addColumn_cell line 318
  35. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.addColumn_new line 320
  36. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.wiring_step line 322
  37. def OAI.CriticalStrip.Diagram.ColumnRectangle.flatten line 396
  38. def OAI.CriticalStrip.Diagram.ColumnRectangle.entries line 401
  39. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.ofFn_entries line 405
  40. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.flatten_boundary line 410
  41. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.active_entries line 414
  42. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.flatten_wiring line 418
  43. def OAI.CriticalStrip.Diagram.ColumnRectangle.boundaryEquiv line 444
  44. lemma OAI.CriticalStrip.Diagram.ColumnRectangle.runs_iff line 449