OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortScheduleTape.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The computed port paths decorate the actual full bond list with its remaining subdivision work. Erasing that work leaves the same Hamiltonian.

  1. abbrev OAI.ContinuumCoulomb.QuantumPortScheduleTape.Environment line 13
  2. def OAI.ContinuumCoulomb.QuantumPortScheduleTape.environmentCode line 14
  3. def OAI.ContinuumCoulomb.QuantumPortScheduleTape.queryCode line 16
  4. def OAI.ContinuumCoulomb.QuantumPortScheduleTape.entry line 18
  5. opaque OAI.ContinuumCoulomb.QuantumPortScheduleTape.entryProgram line 21
  6. def OAI.ContinuumCoulomb.QuantumPortScheduleTape.entries line 33
  7. opaque OAI.ContinuumCoulomb.QuantumPortScheduleTape.entriesProgram line 36
  8. theorem OAI.ContinuumCoulomb.QuantumPortScheduleTape.erase_entries line 45
  9. theorem OAI.ContinuumCoulomb.QuantumPortScheduleTape.entries_ofFn line 52
  10. theorem OAI.ContinuumCoulomb.QuantumPortScheduleTape.allRouted_actual line 62
  11. def OAI.ContinuumCoulomb.QuantumPortScheduleTape.value line 79
  12. opaque OAI.ContinuumCoulomb.QuantumPortScheduleTape.program line 85
  13. theorem OAI.ContinuumCoulomb.QuantumPortScheduleTape.value_erase line 102
  14. theorem OAI.ContinuumCoulomb.QuantumPortScheduleTape.value_valid line 106
  15. theorem OAI.ContinuumCoulomb.QuantumPortScheduleTape.value_energy line 116