OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortCrossingSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Select and remove the actual finite crossing cells in a completed rational port graph. The gadget terminals are existing physical spins.

  1. def OAI.ContinuumCoulomb.qmaPatchDirection line 13
  2. theorem OAI.ContinuumCoulomb.qmaPatchDirection_injective line 15
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.crossingCell line 20
  4. def OAI.ContinuumCoulomb.QMAPortRouteData.crossingSiteFin line 22
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingSiteFin_injective line 26
  6. def OAI.ContinuumCoulomb.QMAPortRouteData.portCrossingSelection line 33
  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.portCrossing_energy_error line 37
  8. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingCells_card_le line 47