OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListPathStep.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

A calibrated selected-subdivision step acting directly on finite bond lists. The selected list order fixes the labels of every new mediator pair.

  1. abbrev OAI.ContinuumCoulomb.QuantumListPathStep.Input line 12
  2. def OAI.ContinuumCoulomb.QuantumListPathStep.headCode line 13
  3. def OAI.ContinuumCoulomb.QuantumListPathStep.inputCode line 15
  4. abbrev OAI.ContinuumCoulomb.QuantumListPathStep.Output line 17
  5. def OAI.ContinuumCoulomb.QuantumListPathStep.outputCode line 18
  6. def OAI.ContinuumCoulomb.QuantumListPathStep.scaleInput line 20
  7. def OAI.ContinuumCoulomb.QuantumListPathStep.parameters line 22
  8. def OAI.ContinuumCoulomb.QuantumListPathStep.count line 24
  9. def OAI.ContinuumCoulomb.QuantumListPathStep.bonds line 25
  10. def OAI.ContinuumCoulomb.QuantumListPathStep.constant line 26
  11. def OAI.ContinuumCoulomb.QuantumListPathStep.value line 27
  12. opaque OAI.ContinuumCoulomb.QuantumListPathStep.headProgram line 29
  13. opaque OAI.ContinuumCoulomb.QuantumListPathStep.countInputProgram line 30
  14. opaque OAI.ContinuumCoulomb.QuantumListPathStep.parityProgram line 32
  15. opaque OAI.ContinuumCoulomb.QuantumListPathStep.constantsProgram line 34
  16. opaque OAI.ContinuumCoulomb.QuantumListPathStep.listsProgram line 37
  17. opaque OAI.ContinuumCoulomb.QuantumListPathStep.retainedProgram line 39
  18. opaque OAI.ContinuumCoulomb.QuantumListPathStep.selectedProgram line 41
  19. opaque OAI.ContinuumCoulomb.QuantumListPathStep.weightProgram line 43
  20. opaque OAI.ContinuumCoulomb.QuantumListPathStep.weightsProgram line 45
  21. opaque OAI.ContinuumCoulomb.QuantumListPathStep.scaleInputProgram line 48
  22. opaque OAI.ContinuumCoulomb.QuantumListPathStep.parametersProgram line 51
  23. opaque OAI.ContinuumCoulomb.QuantumListPathStep.countProgram line 54
  24. opaque OAI.ContinuumCoulomb.QuantumListPathStep.familyInputProgram line 58
  25. opaque OAI.ContinuumCoulomb.QuantumListPathStep.bondsProgram line 60
  26. opaque OAI.ContinuumCoulomb.QuantumListPathStep.constantProgram line 63
  27. opaque OAI.ContinuumCoulomb.QuantumListPathStep.program line 67
  28. theorem OAI.ContinuumCoulomb.QuantumListPathStep.bonds_bounded line 70
  29. theorem OAI.ContinuumCoulomb.QuantumListPathStep.bonds_noLoops line 80
  30. def OAI.ContinuumCoulomb.QuantumListPathStep.graph line 88