OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteProgram.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial programs for the lattice route length and each route point.

  1. abbrev OAI.ContinuumCoulomb.QuantumRouteCode.Pair line 12
  2. def OAI.ContinuumCoulomb.QuantumRouteCode.pairCode line 13
  3. abbrev OAI.ContinuumCoulomb.QuantumRouteCode.AxisInput line 14
  4. def OAI.ContinuumCoulomb.QuantumRouteCode.axisCode line 15
  5. opaque OAI.ContinuumCoulomb.QuantumRouteCode.distanceProgram line 17
  6. opaque OAI.ContinuumCoulomb.QuantumRouteCode.axisPairProgram line 23
  7. opaque OAI.ContinuumCoulomb.QuantumRouteCode.axisStartProgram line 24
  8. opaque OAI.ContinuumCoulomb.QuantumRouteCode.axisEndProgram line 26
  9. opaque OAI.ContinuumCoulomb.QuantumRouteCode.axisCursorProgram line 28
  10. opaque OAI.ContinuumCoulomb.QuantumRouteCode.axisProgram line 30
  11. abbrev OAI.ContinuumCoulomb.QuantumRouteCode.RouteInput line 36
  12. def OAI.ContinuumCoulomb.QuantumRouteCode.routeCode line 37
  13. opaque OAI.ContinuumCoulomb.QuantumRouteCode.endsProgram line 38
  14. opaque OAI.ContinuumCoulomb.QuantumRouteCode.startProgram line 40
  15. opaque OAI.ContinuumCoulomb.QuantumRouteCode.endProgram line 42
  16. opaque OAI.ContinuumCoulomb.QuantumRouteCode.cursorProgram line 44
  17. opaque OAI.ContinuumCoulomb.QuantumRouteCode.startXProgram line 45
  18. opaque OAI.ContinuumCoulomb.QuantumRouteCode.startYProgram line 47
  19. opaque OAI.ContinuumCoulomb.QuantumRouteCode.endXProgram line 49
  20. opaque OAI.ContinuumCoulomb.QuantumRouteCode.endYProgram line 51
  21. opaque OAI.ContinuumCoulomb.QuantumRouteCode.horizontalLengthProgram line 53
  22. opaque OAI.ContinuumCoulomb.QuantumRouteCode.verticalLengthProgram line 56
  23. opaque OAI.ContinuumCoulomb.QuantumRouteCode.lengthProgram line 59
  24. opaque OAI.ContinuumCoulomb.QuantumRouteCode.horizontalPointProgram line 63
  25. opaque OAI.ContinuumCoulomb.QuantumRouteCode.verticalPointProgram line 66
  26. opaque OAI.ContinuumCoulomb.QuantumRouteCode.pointProgram line 71
  27. def OAI.ContinuumCoulomb.QuantumRouteCode.pointCertificate line 77
  28. def OAI.ContinuumCoulomb.QuantumRouteCode.lengthCertificate line 79