OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellPathProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal rational-register-free programs evaluate all four finite cell path families, including the two translated halves of an external corridor.

  1. abbrev OAI.ContinuumCoulomb.QuantumCellPathProgram.TranslateInput line 14
  2. def OAI.ContinuumCoulomb.QuantumCellPathProgram.translateCode line 15
  3. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.translateProgram line 17
  4. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.translatedPathProgram line 30
  5. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.neighborProgram line 35
  6. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.rayProgram line 53
  7. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.pairProgram line 56
  8. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.patchProgram line 59
  9. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.halfProgram line 69
  10. opaque OAI.ContinuumCoulomb.QuantumCellPathProgram.corridorProgram line 72