OAI/Combinatorics/StripMass/TripleCircuit.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. structure OAI.CriticalStrip.Diagram.TriplePosition line 14
  2. lemma OAI.CriticalStrip.Diagram.TriplePosition.ab line 24
  3. lemma OAI.CriticalStrip.Diagram.TriplePosition.bc line 25
  4. lemma OAI.CriticalStrip.Diagram.TriplePosition.ac line 26
  5. def OAI.CriticalStrip.Diagram.TriplePosition.left line 28
  6. def OAI.CriticalStrip.Diagram.TriplePosition.right line 29
  7. def OAI.CriticalStrip.Diagram.TriplePosition.rightCircuit line 31
  8. def OAI.CriticalStrip.Diagram.TriplePosition.vertexEquiv line 34
  9. def OAI.CriticalStrip.Diagram.TriplePosition.wiring line 39
  10. def OAI.CriticalStrip.Diagram.TriplePosition.boundary line 47
  11. lemma OAI.CriticalStrip.Diagram.TriplePosition.vertex_old line 50
  12. lemma OAI.CriticalStrip.Diagram.TriplePosition.vertex_zero line 51
  13. lemma OAI.CriticalStrip.Diagram.TriplePosition.vertex_one line 53
  14. lemma OAI.CriticalStrip.Diagram.TriplePosition.vertex_two line 55
  15. lemma OAI.CriticalStrip.Diagram.TriplePosition.boundary_eq line 58
  16. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_0_0 line 65
  17. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_0_1 line 71
  18. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_0_2 line 80
  19. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_0_3 line 90
  20. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_1_0 line 100
  21. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_1_1 line 109
  22. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_1_2 line 118
  23. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_1_3 line 130
  24. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_2_0 line 142
  25. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_2_1 line 152
  26. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_2_2 line 164
  27. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_2_3 line 173
  28. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_3_0 line 185
  29. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_3_1 line 195
  30. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_3_2 line 207
  31. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_3_3 line 219
  32. lemma OAI.CriticalStrip.Diagram.TriplePosition.edge_iff line 228
  33. lemma OAI.CriticalStrip.Diagram.CompactGate.output_used line 259
  34. lemma OAI.CriticalStrip.Diagram.CompactGate.passed_used line 267
  35. lemma OAI.CriticalStrip.Diagram.CompactGate.boundary_used line 275
  36. lemma OAI.CriticalStrip.Diagram.Circuit.compact_boundary_used line 293
  37. instance OAI.CriticalStrip.Diagram.ThreeBox.adjStdSymm line 308
  38. instance OAI.CriticalStrip.Diagram.TriplePosition.wiring_symm line 313
  39. def OAI.CriticalStrip.Diagram.TriplePosition.equiv line 321
  40. lemma OAI.CriticalStrip.Diagram.TriplePosition.boundary_injective line 326
  41. def OAI.CriticalStrip.Diagram.TriplePosition.support line 333
  42. lemma OAI.CriticalStrip.Diagram.TriplePosition.circuit_support line 337
  43. lemma OAI.CriticalStrip.Diagram.TriplePosition.boundary_used line 343
  44. lemma OAI.CriticalStrip.Diagram.TriplePosition.compatible_iff line 354
  45. lemma OAI.CriticalStrip.Diagram.TriplePosition.eval_iff line 362
  46. def OAI.CriticalStrip.Diagram.Graph.Attached.wiring line 380
  47. def OAI.CriticalStrip.Diagram.Graph.Attached.project line 386
  48. instance OAI.CriticalStrip.Diagram.Graph.Attached.wiring_symm line 390
  49. lemma OAI.CriticalStrip.Diagram.Graph.Attached.map_used line 401
  50. def OAI.CriticalStrip.Diagram.Graph.Attached.contraction line 409
  51. def OAI.CriticalStrip.Diagram.TriplePosition.interface line 446
  52. def OAI.CriticalStrip.Diagram.TriplePosition.active line 449
  53. def OAI.CriticalStrip.Diagram.TriplePosition.exterior line 453
  54. def OAI.CriticalStrip.Diagram.TriplePosition.Outside line 458
  55. def OAI.CriticalStrip.Diagram.TriplePosition.attached line 461
  56. def OAI.CriticalStrip.Diagram.TriplePosition.patch line 464
  57. def OAI.CriticalStrip.Diagram.TriplePosition.exteriorEquiv line 467
  58. lemma OAI.CriticalStrip.Diagram.TriplePosition.boundary_old line 479
  59. lemma OAI.CriticalStrip.Diagram.TriplePosition.boundary_new line 485
  60. lemma OAI.CriticalStrip.Diagram.TriplePosition.interface_old line 492
  61. lemma OAI.CriticalStrip.Diagram.TriplePosition.interface_new line 501
  62. lemma OAI.CriticalStrip.Diagram.TriplePosition.exterior_edge line 517