OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortChainProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Literal evaluation of the physical port chain on a computed coarse path. The output enumerates both endpoint centers and every incoming/outgoing port.

  1. def OAI.ContinuumCoulomb.QuantumPortChainProgram.offset line 14
  2. def OAI.ContinuumCoulomb.QuantumPortChainProgram.offsetProgram line 16
  3. def OAI.ContinuumCoulomb.QuantumPortChainProgram.port line 28
  4. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.port_fin line 32
  5. def OAI.ContinuumCoulomb.QuantumPortChainProgram.portProgram line 35
  6. def OAI.ContinuumCoulomb.QuantumPortChainProgram.directedProgram line 47
  7. def OAI.ContinuumCoulomb.QuantumPortChainProgram.centerProgram line 54
  8. def OAI.ContinuumCoulomb.QuantumPortChainProgram.neighborProgram line 57
  9. abbrev OAI.ContinuumCoulomb.QuantumPortChainProgram.Input line 69
  10. def OAI.ContinuumCoulomb.QuantumPortChainProgram.inputCode line 70
  11. def OAI.ContinuumCoulomb.QuantumPortChainProgram.point line 72
  12. def OAI.ContinuumCoulomb.QuantumPortChainProgram.lengthProgram line 75
  13. def OAI.ContinuumCoulomb.QuantumPortChainProgram.pointProgram line 81
  14. def OAI.ContinuumCoulomb.QuantumPortChainProgram.value line 102
  15. theorem OAI.ContinuumCoulomb.QuantumPortChainProgram.value_length line 105
  16. def OAI.ContinuumCoulomb.QuantumPortChainProgram.program line 108