OAI/Combinatorics/StripMass/WireContraction.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. structure OAI.CriticalStrip.Diagram.Graph.WireContraction line 17
  2. theorem OAI.CriticalStrip.Diagram.Graph.WireContraction.lift_boundary_reach line 34
  3. theorem OAI.CriticalStrip.Diagram.Graph.WireContraction.realizes line 43
  4. theorem OAI.CriticalStrip.Diagram.Graph.WireContraction.realizes_inv line 61
  5. theorem OAI.CriticalStrip.Diagram.Graph.WireContraction.realizes_iff line 82
  6. def OAI.CriticalStrip.Diagram.CompactGate.wiring line 98
  7. def OAI.CriticalStrip.Diagram.CompactGate.boundary line 105
  8. def OAI.CriticalStrip.Diagram.CompactGate.project line 108
  9. def OAI.CriticalStrip.Diagram.CompactGate.core line 113
  10. theorem OAI.CriticalStrip.Diagram.CompactGate.project_core line 117
  11. theorem OAI.CriticalStrip.Diagram.CompactGate.boundary_left line 120
  12. theorem OAI.CriticalStrip.Diagram.CompactGate.boundary_right line 122
  13. theorem OAI.CriticalStrip.Diagram.CompactGate.boundary_injective line 125
  14. instance OAI.CriticalStrip.Diagram.CompactGate.wiring_symm line 133
  15. instance OAI.CriticalStrip.Diagram.Patch.glued_symm line 145
  16. instance OAI.CriticalStrip.Diagram.gateWiring_symm line 161
  17. abbrev OAI.CriticalStrip.Diagram.CompactGate.full line 171
  18. lemma OAI.CriticalStrip.Diagram.CompactGate.core_edge line 175
  19. lemma OAI.CriticalStrip.Diagram.CompactGate.project_edge line 194
  20. lemma OAI.CriticalStrip.Diagram.CompactGate.used_old_iff line 225
  21. lemma OAI.CriticalStrip.Diagram.CompactGate.used_output_iff line 239
  22. lemma OAI.CriticalStrip.Diagram.CompactGate.output_edge line 266
  23. lemma OAI.CriticalStrip.Diagram.CompactGate.full_used_out line 282
  24. lemma OAI.CriticalStrip.Diagram.CompactGate.project_used line 296
  25. def OAI.CriticalStrip.Diagram.CompactGate.contraction line 319
  26. theorem OAI.CriticalStrip.Diagram.CompactGate.realizes_iff line 340
  27. lemma OAI.CriticalStrip.Diagram.Graph.used_of_reach line 353
  28. lemma OAI.CriticalStrip.Diagram.Graph.WireContraction.drains line 359
  29. lemma OAI.CriticalStrip.Diagram.Graph.WireContraction.drains_inv line 368
  30. lemma OAI.CriticalStrip.Diagram.Graph.WireContraction.drains_iff line 378
  31. def OAI.CriticalStrip.Diagram.CompactGate.localEnd line 393
  32. lemma OAI.CriticalStrip.Diagram.CompactGate.reach_exit line 397
  33. lemma OAI.CriticalStrip.Diagram.CompactGate.drains_local line 416
  34. def OAI.CriticalStrip.Diagram.Circuit.CompactVertex line 434
  35. def OAI.CriticalStrip.Diagram.Circuit.compactBoundary line 438
  36. def OAI.CriticalStrip.Diagram.Circuit.compactWiring line 442
  37. theorem OAI.CriticalStrip.Diagram.Circuit.compactBoundary_injective line 447
  38. instance OAI.CriticalStrip.Diagram.Circuit.compactWiring_symm line 452
  39. theorem OAI.CriticalStrip.Diagram.Circuit.compact_eval_sound line 459
  40. theorem OAI.CriticalStrip.Diagram.Circuit.compact_eval_exists line 477
  41. theorem OAI.CriticalStrip.Diagram.Circuit.compact_eval_iff line 498