OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenRouteData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Even route lengths use one singlet leaf. The leaf sits beside the first interior route point and outside all routed edges.

  1. structure OAI.ContinuumCoulomb.QMAEvenRouteData line 13
  2. def OAI.ContinuumCoulomb.QMAEvenRouteData.selected line 34
  3. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.selected_injective line 37
  4. def OAI.ContinuumCoulomb.QMAEvenRouteData.freshPosition line 42
  5. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.freshPosition_ne_old line 45
  6. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.freshPosition_injective line 51
  7. def OAI.ContinuumCoulomb.QMAEvenRouteData.nextPosition line 69
  8. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPosition_old line 72
  9. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPosition_fresh line 75
  10. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPosition_injective line 79
  11. def OAI.ContinuumCoulomb.QMAEvenRouteData.nextWork line 95
  12. def OAI.ContinuumCoulomb.QMAEvenRouteData.schedule line 100
  13. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.schedule_work_le line 104
  14. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.schedule_energy_error line 115