OAI/Combinatorics/StripMass/FreshGate.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. structure OAI.CriticalStrip.Diagram.FreshGate.Ports line 17
  2. def OAI.CriticalStrip.Diagram.FreshGate.Ports.project line 28
  3. def OAI.CriticalStrip.Diagram.FreshGate.Ports.core line 32
  4. theorem OAI.CriticalStrip.Diagram.FreshGate.Ports.project_core line 35
  5. theorem OAI.CriticalStrip.Diagram.FreshGate.Ports.core_port line 40
  6. theorem OAI.CriticalStrip.Diagram.FreshGate.Ports.core_old line 41
  7. def OAI.CriticalStrip.Diagram.FreshGate.Ports.boundary line 43
  8. def OAI.CriticalStrip.Diagram.FreshGate.Ports.wiring line 45
  9. lemma OAI.CriticalStrip.Diagram.FreshGate.Ports.core_boundary line 48
  10. lemma OAI.CriticalStrip.Diagram.FreshGate.Ports.core_project_used line 52
  11. instance OAI.CriticalStrip.Diagram.FreshGate.Ports.wiring_symm line 66
  12. def OAI.CriticalStrip.Diagram.FreshGate.Ports.contraction line 74
  13. theorem OAI.CriticalStrip.Diagram.FreshGate.Ports.realizes_iff line 109
  14. abbrev OAI.CriticalStrip.Diagram.PartialColumn.V line 119
  15. def OAI.CriticalStrip.Diagram.PartialColumn.wiring line 121
  16. def OAI.CriticalStrip.Diagram.PartialColumn.boundary line 130
  17. def OAI.CriticalStrip.Diagram.PartialColumn.support line 135
  18. theorem OAI.CriticalStrip.Diagram.PartialColumn.boundary_zero line 141
  19. theorem OAI.CriticalStrip.Diagram.PartialColumn.support_zero line 143
  20. instance OAI.CriticalStrip.Diagram.PartialColumn.wiring_symm line 146
  21. theorem OAI.CriticalStrip.Diagram.PartialColumn.boundary_injective line 158
  22. def OAI.CriticalStrip.Diagram.PartialColumn.select line 165
  23. def OAI.CriticalStrip.Diagram.PartialColumn.ports line 169
  24. def OAI.CriticalStrip.Diagram.PartialColumn.prev line 214
  25. lemma OAI.CriticalStrip.Diagram.PartialColumn.right_boundary line 216
  26. lemma OAI.CriticalStrip.Diagram.PartialColumn.left_boundary_zero line 219
  27. lemma OAI.CriticalStrip.Diagram.PartialColumn.left_boundary_pos line 223
  28. lemma OAI.CriticalStrip.Diagram.PartialColumn.right_support line 227
  29. lemma OAI.CriticalStrip.Diagram.PartialColumn.left_support_zero line 230
  30. lemma OAI.CriticalStrip.Diagram.PartialColumn.left_support_pos line 235
  31. lemma OAI.CriticalStrip.Diagram.PartialColumn.boundary_step line 239
  32. lemma OAI.CriticalStrip.Diagram.PartialColumn.support_step line 257
  33. lemma OAI.CriticalStrip.Diagram.PartialColumn.core_initial line 274
  34. lemma OAI.CriticalStrip.Diagram.PartialColumn.core_box line 275
  35. abbrev OAI.CriticalStrip.Diagram.PartialColumn.nextWiring line 279
  36. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_initial line 282
  37. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_mixed line 286
  38. lemma OAI.CriticalStrip.Diagram.PartialColumn.prev_val_add line 302
  39. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_new_new line 306
  40. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_new_old line 311
  41. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_old_old line 337
  42. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_iff line 346
  43. lemma OAI.CriticalStrip.Diagram.PartialColumn.next_eq line 365
  44. def OAI.CriticalStrip.Diagram.PartialColumn.fullBoundary line 373
  45. def OAI.CriticalStrip.Diagram.PartialColumn.fullProject line 376
  46. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_box line 380
  47. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_initial_zero line 387
  48. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_mixed line 394
  49. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_map_edge line 400
  50. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_inv_edge line 415
  51. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_map_used line 427
  52. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_inv_used line 445
  53. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_boundary line 455
  54. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_retract line 460
  55. def OAI.CriticalStrip.Diagram.PartialColumn.fullEquiv line 477