OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumMergedOutputRoutes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact parallel-edge merging preserves the physical placement and reverses the catalog route when canonical endpoint ordering requires it.

  1. def OAI.ContinuumCoulomb.QMACellRoute.reverse line 15
  2. theorem OAI.ContinuumCoulomb.QMACellRoute.reverse_body line 17
  3. theorem OAI.ContinuumCoulomb.QMACellRoute.reverse_source line 19
  4. theorem OAI.ContinuumCoulomb.QMACellRoute.reverse_target line 23
  5. theorem OAI.ContinuumCoulomb.QMACellRoute.reverse_valid line 27
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.mergedOutput_route_exists line 33
  7. def OAI.ContinuumCoulomb.QMAPortRouteData.findMergedRoute line 48
  8. theorem OAI.ContinuumCoulomb.QMAPortRouteData.findMergedRoute_isSome line 57
  9. theorem OAI.ContinuumCoulomb.QMAPortRouteData.findMergedRoute_spec line 66
  10. def OAI.ContinuumCoulomb.QMAPortRouteData.mergedOutputRoute line 77
  11. theorem OAI.ContinuumCoulomb.QMAPortRouteData.mergedOutputRoute_spec line 82
  12. theorem OAI.ContinuumCoulomb.QMAPortRouteData.mergedOutput_energy_error line 94