OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteSelectorCorrectness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite data program returns exactly the path used by the actual merged physical graph, rather than merely a path with the same endpoints.

  1. theorem OAI.ContinuumCoulomb.QMACellRoute.headD_path line 18
  2. theorem OAI.ContinuumCoulomb.QMACellRoute.reverse_headD_path line 22
  3. theorem OAI.ContinuumCoulomb.QMAPortRouteData.routing_accepts line 31
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.selected_merged_path line 44