OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumInnerPorts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Moving crossing terminals one unit into their private patch leaves the external corridors free and creates space for the two mediator spins.

  1. def OAI.ContinuumCoulomb.qmaInnerPort line 10
  2. def OAI.ContinuumCoulomb.qmaGadgetAncilla line 14
  3. theorem OAI.ContinuumCoulomb.qmaInnerPort_cell line 17
  4. theorem OAI.ContinuumCoulomb.qmaGadgetAncilla_cell line 21
  5. theorem OAI.ContinuumCoulomb.qmaExpandedPoint_cell line 25
  6. theorem OAI.ContinuumCoulomb.qmaInnerPort_injective line 29
  7. theorem OAI.ContinuumCoulomb.qmaGadgetAncilla_injective line 41
  8. theorem OAI.ContinuumCoulomb.qmaInnerPort_ne_center line 52
  9. theorem OAI.ContinuumCoulomb.qmaInnerPort_ne_port line 59
  10. theorem OAI.ContinuumCoulomb.qmaGadgetAncilla_ne_center line 66
  11. theorem OAI.ContinuumCoulomb.qmaGadgetAncilla_ne_port line 72
  12. theorem OAI.ContinuumCoulomb.qmaGadgetAncilla_ne_inner line 78
  13. def OAI.ContinuumCoulomb.qmaPortIndex line 84
  14. theorem OAI.ContinuumCoulomb.qmaPortIndex_spec line 87
  15. def OAI.ContinuumCoulomb.qmaCrossingMove line 90
  16. theorem OAI.ContinuumCoulomb.qmaCrossingMove_center line 94
  17. theorem OAI.ContinuumCoulomb.qmaCrossingMove_port line 98