OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactSourceInputProgram.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

A literal polynomial-time program turns the source coordinate/bond lists and calibrated final-edge lengths into all rational contact sites.

  1. abbrev OAI.ContinuumCoulomb.ContactSourceInputProgram.Input line 14
  2. def OAI.ContinuumCoulomb.ContactSourceInputProgram.inputCode line 16
  3. abbrev OAI.ContinuumCoulomb.ContactSourceInputProgram.LoopInput line 20
  4. def OAI.ContinuumCoulomb.ContactSourceInputProgram.loopCode line 22
  5. def OAI.ContinuumCoulomb.ContactSourceInputProgram.bond line 24
  6. def OAI.ContinuumCoulomb.ContactSourceInputProgram.edge line 27
  7. def OAI.ContinuumCoulomb.ContactSourceInputProgram.edges line 33
  8. def OAI.ContinuumCoulomb.ContactSourceInputProgram.positions line 36
  9. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.indexProgram line 39
  10. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.inputProgram line 42
  11. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.precisionProgram line 45
  12. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.dataProgram line 48
  13. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.coordinatesProgram line 53
  14. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.listsProgram line 57
  15. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.bondsProgram line 61
  16. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.lengthsProgram line 65
  17. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.countProgram line 68
  18. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.bondProgram line 72
  19. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.leftIndexProgram line 76
  20. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.bondTailProgram line 79
  21. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.rightIndexProgram line 82
  22. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.weightProgram line 85
  23. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.signProgram line 88
  24. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.leftProgram line 94
  25. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.rightProgram line 99
  26. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.localProgram line 104
  27. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.edgeProgram line 110
  28. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.edgesProgram line 113
  29. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.program line 125
  30. def OAI.ContinuumCoulomb.ContactSourceInputProgram.certificate line 130
  31. def OAI.ContinuumCoulomb.ContactSourceInputProgram.scaledInputCode line 133
  32. def OAI.ContinuumCoulomb.ContactSourceInputProgram.scalePoint line 135
  33. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.scalePointProgram line 137
  34. def OAI.ContinuumCoulomb.ContactSourceInputProgram.scaledPositions line 145
  35. opaque OAI.ContinuumCoulomb.ContactSourceInputProgram.scaledProgram line 148
  36. def OAI.ContinuumCoulomb.ContactSourceInputProgram.scaledCertificate line 156