OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingPositionProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Literal physical coordinates after crossing removal. Only ports in the computed crossing cells move; the two fresh spins use fixed local coordinates.

  1. abbrev OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.Input line 16
  2. def OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.inputCode line 17
  3. def OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.cell line 18
  4. def OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.move line 19
  5. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.cellProgram line 21
  6. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.innerProgram line 26
  7. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.ancillaProgram line 34
  8. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.chosenInnerProgram line 42
  9. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.moveProgram line 60
  10. def OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.moved line 74
  11. def OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.fresh line 75
  12. def OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.positions line 77
  13. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.movedProgram line 79
  14. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.freshProgram line 83
  15. opaque OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.positionsProgram line 90
  16. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.move_eq line 95
  17. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.moved_ofFn line 100
  18. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.fresh_length line 105
  19. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.positions_length line 110
  20. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.moved_actual line 114
  21. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.fresh_actual line 119
  22. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.crossingPosition_list line 124
  23. theorem OAI.ContinuumCoulomb.QuantumCrossingPositionProgram.positions_actual line 153