OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialPortProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal fixed-round realization of the computed spatial graph on its port paths. The finite tape carries the actual spin positions throughout subdivision.

  1. abbrev OAI.ContinuumCoulomb.QuantumSpatialPortProgram.Input line 14
  2. def OAI.ContinuumCoulomb.QuantumSpatialPortProgram.inputCode line 15
  3. def OAI.ContinuumCoulomb.QuantumSpatialPortProgram.initial line 17
  4. opaque OAI.ContinuumCoulomb.QuantumSpatialPortProgram.roundValue line 22
  5. def OAI.ContinuumCoulomb.QuantumSpatialPortProgram.rounds line 25
  6. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.rounds_eq line 26
  7. def OAI.ContinuumCoulomb.QuantumSpatialPortProgram.value line 30
  8. opaque OAI.ContinuumCoulomb.QuantumSpatialPortProgram.initialProgram line 33
  9. opaque OAI.ContinuumCoulomb.QuantumSpatialPortProgram.program line 39
  10. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.initial_bounded line 49
  11. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.initial_work line 74
  12. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.realizes line 83