OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenTapeProgram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

One literal even subdivision, with its reserved leaf and odd route tails.

  1. abbrev OAI.ContinuumCoulomb.QuantumEvenTapeProgram.Input line 13
  2. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.inputCode line 14
  3. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.stepInput line 15
  4. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.route line 17
  5. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.blockInput line 18
  6. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.entries line 21
  7. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.positions line 23
  8. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.paths line 25
  9. def OAI.ContinuumCoulomb.QuantumEvenTapeProgram.value line 26
  10. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.precisionProgram line 30
  11. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.dataProgram line 31
  12. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.packetProgram line 33
  13. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.geometryProgram line 35
  14. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.countProgram line 38
  15. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.bondsProgram line 40
  16. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.constantProgram line 43
  17. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.oldPositionsProgram line 46
  18. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.oldPathsProgram line 48
  19. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.stepInputProgram line 50
  20. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.routeProgram line 55
  21. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.workProgram line 60
  22. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.blockInputProgram line 65
  23. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.blockProgram line 73
  24. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.entriesTabProgram line 77
  25. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.bondCountProgram line 81
  26. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.entriesNestedProgram line 84
  27. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.entriesProgram line 90
  28. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.positionsProgram line 95
  29. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.pathsProgram line 100
  30. opaque OAI.ContinuumCoulomb.QuantumEvenTapeProgram.program line 103
  31. theorem OAI.ContinuumCoulomb.QuantumEvenTapeProgram.erase_entries line 108
  32. theorem OAI.ContinuumCoulomb.QuantumEvenTapeProgram.value_valid line 117
  33. theorem OAI.ContinuumCoulomb.QuantumEvenTapeProgram.value_energy_error line 130