OAI/Combinatorics/StripMass/CutStateSound.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.tileStep_sound_vacant line 16
  2. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_sound_single₀ line 32
  3. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_sound_single₁ line 52
  4. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_sound_paired line 72
  5. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_sound_separate line 88
  6. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_sound line 105
  7. theorem OAI.CriticalStrip.Diagram.Pairing.adj_trans_eq line 131
  8. theorem OAI.CriticalStrip.Diagram.Pairing.reach_adj_iff line 135
  9. theorem OAI.CriticalStrip.Diagram.Patch.pairing_adj_compressed line 162
  10. theorem OAI.CriticalStrip.Diagram.Patch.compressed_pairing line 169
  11. theorem OAI.CriticalStrip.Diagram.Patch.compressed_reach_pairing line 181
  12. theorem OAI.CriticalStrip.Diagram.Patch.compressed_drains_pairing line 197
  13. theorem OAI.CriticalStrip.Diagram.Patch.glued_reach_pairing line 202
  14. theorem OAI.CriticalStrip.Diagram.Patch.glued_drains_pairing line 208
  15. structure OAI.CriticalStrip.Diagram.GraphRealizes line 223
  16. theorem OAI.CriticalStrip.Diagram.CutPatch.Realizes.reach line 230
  17. theorem OAI.CriticalStrip.Diagram.CutPatch.Realizes.edge_active line 239
  18. def OAI.CriticalStrip.Diagram.Pairing.cutGraph line 249
  19. theorem OAI.CriticalStrip.Diagram.Pairing.cutGraph_realizes line 254
  20. def OAI.CriticalStrip.Diagram.Graph.Used line 294
  21. theorem OAI.CriticalStrip.Diagram.Graph.map_reach line 296
  22. structure OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv line 305
  23. def OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv.symm line 322
  24. theorem OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv.realizes line 326
  25. theorem OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv.realizes_iff line 346
  26. inductive OAI.CriticalStrip.Diagram.StepVertex line 360
  27. def OAI.CriticalStrip.Diagram.Pairing.stepWiring line 368
  28. def OAI.CriticalStrip.Diagram.Pairing.stepToCut line 380
  29. def OAI.CriticalStrip.Diagram.Pairing.cutToStep line 385
  30. theorem OAI.CriticalStrip.Diagram.Pairing.stepWiring_symm line 389
  31. instance OAI.CriticalStrip.Diagram.Pairing.stepWiring_isSymm line 395
  32. theorem OAI.CriticalStrip.Diagram.Pairing.cutGraph_symm line 398
  33. instance OAI.CriticalStrip.Diagram.Pairing.cutGraph_isSymm line 410
  34. theorem OAI.CriticalStrip.Diagram.CutPatch.active_zero line 417
  35. theorem OAI.CriticalStrip.Diagram.CutPatch.active_one line 420
  36. theorem OAI.CriticalStrip.Diagram.CutPatch.active_two line 423
  37. theorem OAI.CriticalStrip.Diagram.CutPatch.active_three line 426
  38. theorem OAI.CriticalStrip.Diagram.CutPatch.input_occupied_zero line 429
  39. theorem OAI.CriticalStrip.Diagram.CutPatch.input_occupied_one line 432
  40. theorem OAI.CriticalStrip.Diagram.Pairing.cutShape_input_zero line 439
  41. theorem OAI.CriticalStrip.Diagram.Pairing.cutShape_input_one line 445
  42. theorem OAI.CriticalStrip.Diagram.Pairing.cutShape_compatible line 451
  43. theorem OAI.CriticalStrip.Diagram.Pairing.cutShape_active_two line 457
  44. theorem OAI.CriticalStrip.Diagram.Pairing.cutShape_active_three line 464