OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactHeightScheduleProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time execution of the concrete contact-height search. All precision and iteration counts are unary linear functions of the request.

  1. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.envPrecisionProgram line 12
  2. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.envDataProgram line 15
  3. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.refinedPrecisionProgram line 19
  4. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.refinedProgram line 23
  5. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.iterationProgram line 26
  6. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.toleranceProgram line 29
  7. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.scheduledArgumentProgram line 38
  8. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.scheduledProgram line 45
  9. def OAI.ContinuumCoulomb.ContactHeightEvaluation.scheduledCertificate line 49