OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingPairSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

At a selected crossing, every internal port edge is one of its two opposite pairs. This excludes leftover crossed interactions after edge selection.

  1. theorem OAI.ContinuumCoulomb.QMAPortRouteData.cell_visits_third line 14
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossing_graph_pair line 29