OAI/MathematicalPhysics/ContinuumCoulomb/Programs/HoppingProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A literal polynomial TM2 program for the contact numerator, with unary displacement bound and inverse-accuracy parameter.

  1. def OAI.ContinuumCoulomb.HoppingSchedule.inputCode line 12
  2. opaque OAI.ContinuumCoulomb.HoppingSchedule.meshFactorsProgram line 14
  3. opaque OAI.ContinuumCoulomb.HoppingSchedule.meshRawProgram line 18
  4. opaque OAI.ContinuumCoulomb.HoppingSchedule.meshProgram line 21
  5. opaque OAI.ContinuumCoulomb.HoppingSchedule.accuracyProgram line 24
  6. opaque OAI.ContinuumCoulomb.HoppingSchedule.argumentProgram line 27
  7. opaque OAI.ContinuumCoulomb.HoppingSchedule.program line 41
  8. def OAI.ContinuumCoulomb.HoppingSchedule.certificate line 44