OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CalibratedContactProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

One literal polynomial-time map from source arrays and target edge coefficients to the physically scaled rational contact coordinates.

  1. abbrev OAI.ContinuumCoulomb.CalibratedContactProgram.Data line 13
  2. abbrev OAI.ContinuumCoulomb.CalibratedContactProgram.Input line 14
  3. def OAI.ContinuumCoulomb.CalibratedContactProgram.dataCode line 16
  4. def OAI.ContinuumCoulomb.CalibratedContactProgram.inputCode line 20
  5. def OAI.ContinuumCoulomb.CalibratedContactProgram.rawInput line 23
  6. def OAI.ContinuumCoulomb.CalibratedContactProgram.value line 27
  7. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.precisionProgram line 31
  8. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.restProgram line 34
  9. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.environmentProgram line 37
  10. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.dataProgram line 41
  11. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.coordinatesProgram line 44
  12. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.listsProgram line 48
  13. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.bondsProgram line 52
  14. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.coefficientsProgram line 56
  15. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.lengthsProgram line 59
  16. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.rawProgram line 65
  17. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.spacingProgram line 70
  18. opaque OAI.ContinuumCoulomb.CalibratedContactProgram.program line 75
  19. def OAI.ContinuumCoulomb.CalibratedContactProgram.certificate line 80