OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingPlacement.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Injective physical placement for every spin after simultaneous crossing removal.

  1. def OAI.ContinuumCoulomb.QMAPortRouteData.movedPosition line 15
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.movedPosition_injective line 18
  3. theorem OAI.ContinuumCoulomb.QMAPortRouteData.movedPosition_site line 24
  4. def OAI.ContinuumCoulomb.QMAPortRouteData.freshCrossingPosition line 29
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.freshCrossingPosition_injective line 32
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.freshCrossingPosition_ne_old line 42
  7. def OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition line 46
  8. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition_old line 51
  9. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition_fresh line 55
  10. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition_injective line 59