OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingSiteProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Locate crossing terminals by scanning the actual physical position tape. The finite search returns exactly the existing terminal spin indices.

  1. abbrev OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.Input line 15
  2. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.inputCode line 16
  3. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.flags line 17
  4. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.index line 18
  5. opaque OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.flagsProgram line 20
  6. opaque OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.indexProgram line 27
  7. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.index_eq line 30
  8. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.index_ofFn line 34
  9. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.target line 46
  10. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.terminal line 48
  11. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.sites line 49
  12. opaque OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.targetProgram line 51
  13. opaque OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.terminalProgram line 57
  14. opaque OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.sitesProgram line 59
  15. def OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.allSites line 63
  16. opaque OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.allSitesProgram line 64
  17. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.terminal_actual line 68
  18. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.sites_actual line 77
  19. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.allSites_actual line 83