OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactHeightProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

A literal rational height-residual program. It reads nine input lengths and executes four already-certified rational square-root subprograms.

  1. def OAI.ContinuumCoulomb.ContactHeightEvaluation.environmentCode line 13
  2. def OAI.ContinuumCoulomb.ContactHeightEvaluation.inputCode line 16
  3. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.environmentProgram line 18
  4. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.heightProgram line 21
  5. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.precisionProgram line 24
  6. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.dataProgram line 27
  7. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.lengthsProgram line 31
  8. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.targetProgram line 35
  9. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.lengthProgram line 38
  10. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.squareLengthProgram line 43
  11. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.squareHeightProgram line 48
  12. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.radicandProgram line 53
  13. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.rootPrecisionProgram line 57
  14. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.rootProgram line 61
  15. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.axial01Program line 65
  16. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.axial014Program line 69
  17. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.axial0147Program line 73
  18. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.axialProgram line 77
  19. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.firstRootProgram line 81
  20. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.secondRootProgram line 85
  21. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.thirdRootProgram line 90
  22. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.spanProgram line 95
  23. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.program line 100
  24. def OAI.ContinuumCoulomb.ContactHeightEvaluation.certificate line 103