OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellRouteCatalog.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A finite catalog of the four local route types used by the physical graph. Every valid catalog entry is a simple grid path of at most twenty steps.

  1. inductive OAI.ContinuumCoulomb.QMACellRouteBody line 10
  2. def OAI.ContinuumCoulomb.QMACellRouteBody.path line 18
  3. def OAI.ContinuumCoulomb.QMACellRouteBody.source line 24
  4. def OAI.ContinuumCoulomb.QMACellRouteBody.target line 30
  5. def OAI.ContinuumCoulomb.QMACellRouteBody.Valid line 36
  6. theorem OAI.ContinuumCoulomb.QMACellRouteBody.endpoints line 40
  7. theorem OAI.ContinuumCoulomb.QMACellRouteBody.length_bounds line 59
  8. theorem OAI.ContinuumCoulomb.QMACellRouteBody.simple line 72
  9. theorem OAI.ContinuumCoulomb.QMACellRouteBody.chain line 79
  10. structure OAI.ContinuumCoulomb.QMACellRoute line 97
  11. def OAI.ContinuumCoulomb.QMACellRoute.path line 103
  12. def OAI.ContinuumCoulomb.QMACellRoute.source line 104
  13. def OAI.ContinuumCoulomb.QMACellRoute.target line 105
  14. def OAI.ContinuumCoulomb.QMACellRoute.Valid line 106
  15. theorem OAI.ContinuumCoulomb.QMACellRoute.endpoints line 108
  16. theorem OAI.ContinuumCoulomb.QMACellRoute.length_bounds line 116
  17. theorem OAI.ContinuumCoulomb.QMACellRoute.simple line 120
  18. theorem OAI.ContinuumCoulomb.QMACellRoute.chain line 126