OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPermittedRouteSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The complete permitted catalog is planar: different unordered physical endpoint pairs have disjoint path interiors.

  1. theorem OAI.ContinuumCoulomb.qmaCellBody_cases line 13
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.permitted_bodies_disjoint line 24
  3. theorem OAI.ContinuumCoulomb.QMAPortRouteData.permitted_routes_disjoint line 50
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.mergedOutputRoute_disjoint line 59