OAI/Combinatorics/StripMass/StepToCut.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.Pairing.inlinePrivate74_cut_input_left line 16
  2. theorem OAI.CriticalStrip.Diagram.Pairing.inlinePrivate74_cut_input_right line 21
  3. theorem OAI.CriticalStrip.Diagram.Pairing.inlinePrivate74_cut_input_paired line 26
  4. theorem OAI.CriticalStrip.Diagram.Pairing.cutReach_left line 33
  5. theorem OAI.CriticalStrip.Diagram.Pairing.cutReach_right line 48
  6. theorem OAI.CriticalStrip.Diagram.Pairing.cutReach_old_edge line 63
  7. theorem OAI.CriticalStrip.Diagram.Pairing.cutReach_box_output line 84
  8. theorem OAI.CriticalStrip.Diagram.Pairing.cutReach_old_box line 91
  9. theorem OAI.CriticalStrip.Diagram.Pairing.cutReach_old_output line 98
  10. theorem OAI.CriticalStrip.Diagram.Pairing.stepToCut_edge line 105
  11. theorem OAI.CriticalStrip.Diagram.Pairing.cutToStep_tilePort line 131
  12. theorem OAI.CriticalStrip.Diagram.Pairing.partnerOrSelf_occupied line 135
  13. theorem OAI.CriticalStrip.Diagram.Pairing.partnerOrSelf_away_left line 139
  14. theorem OAI.CriticalStrip.Diagram.Pairing.step_input_left line 144
  15. theorem OAI.CriticalStrip.Diagram.Pairing.step_input_right line 150
  16. theorem OAI.CriticalStrip.Diagram.Pairing.step_input_paired line 156
  17. theorem OAI.CriticalStrip.Diagram.Pairing.cut_input_cases line 163
  18. theorem OAI.CriticalStrip.Diagram.Pairing.stepReach_input_edge line 170
  19. theorem OAI.CriticalStrip.Diagram.Pairing.stepReach_interface line 178
  20. theorem OAI.CriticalStrip.Diagram.Pairing.stepReach_omitted line 193
  21. theorem OAI.CriticalStrip.Diagram.Pairing.cutToStep_edge line 202
  22. theorem OAI.CriticalStrip.Diagram.Graph.used_of_reach_ne line 236
  23. theorem OAI.CriticalStrip.Diagram.Tile.adj_irrefl line 244
  24. theorem OAI.CriticalStrip.Diagram.Pairing.stepToCut_old_injective line 249
  25. theorem OAI.CriticalStrip.Diagram.Pairing.cutGraph_used_old line 256
  26. theorem OAI.CriticalStrip.Diagram.Pairing.stepWiring_old_used line 265
  27. theorem OAI.CriticalStrip.Diagram.Pairing.stepToCut_used line 276
  28. theorem OAI.CriticalStrip.Diagram.Pairing.cutToStep_edge_ne line 305
  29. theorem OAI.CriticalStrip.Diagram.Pairing.cutToStep_used line 335
  30. theorem OAI.CriticalStrip.Diagram.CutPatch.adj_four_active line 350
  31. theorem OAI.CriticalStrip.Diagram.CutPatch.adj_five_active line 353
  32. theorem OAI.CriticalStrip.Diagram.Pairing.cutGraph_used_four line 360
  33. theorem OAI.CriticalStrip.Diagram.Pairing.cutGraph_used_five line 369
  34. theorem OAI.CriticalStrip.Diagram.Pairing.stepToCut_retract line 378
  35. theorem OAI.CriticalStrip.Diagram.Pairing.cutToStep_retract line 398
  36. def OAI.CriticalStrip.Diagram.Pairing.stepCutEquiv line 427
  37. theorem OAI.CriticalStrip.Diagram.Pairing.stepWiring_realizes line 440
  38. theorem OAI.CriticalStrip.Diagram.Pairing.ext_adj line 454
  39. theorem OAI.CriticalStrip.Diagram.Pairing.graphRealizes line 471
  40. theorem OAI.CriticalStrip.Diagram.GraphRealizes.unique line 479
  41. theorem OAI.CriticalStrip.Diagram.GraphRealizes.compressed_eq line 490
  42. theorem OAI.CriticalStrip.Diagram.GraphRealizes.drains_glued_iff line 497
  43. theorem OAI.CriticalStrip.Diagram.Patch.realizes_iff_drains line 510
  44. theorem OAI.CriticalStrip.Diagram.GraphRealizes.substitute_iff line 540