OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathVisitCorrectness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The encoded consecutive-point rule recovers the actual directional ports of every interior visit in the proved port-route geometry.

  1. theorem OAI.ContinuumCoulomb.QuantumPathVisitProgram.lookup_range line 13
  2. theorem OAI.ContinuumCoulomb.QuantumPathVisitProgram.both_member line 18
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.routeList line 34
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.routeList_lookup line 37
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.routeList_visit line 41
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.routeList_visits line 49
  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.routeList_visits_general line 67