OAI/MathematicalPhysics/ContinuumCoulomb/Programs/MoserCoordinateProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A deterministic polynomial TM2 program for the actual rounded Moser coordinate construction. The fixed integers U,C occur as hardcoded constants; precision is unary and geometric input data are binary rationals.

  1. abbrev OAI.ContinuumCoulomb.ManufacturedEuler.Input line 16
  2. def OAI.ContinuumCoulomb.ManufacturedEuler.inputCode line 17
  3. def OAI.ContinuumCoulomb.ManufacturedEuler.value line 19
  4. opaque OAI.ContinuumCoulomb.ManufacturedEuler.stepsProgram line 22
  5. opaque OAI.ContinuumCoulomb.ManufacturedEuler.inputStepsProgram line 24
  6. opaque OAI.ContinuumCoulomb.ManufacturedEuler.denominatorProgram line 27
  7. opaque OAI.ContinuumCoulomb.ManufacturedEuler.inputPointProgram line 30
  8. opaque OAI.ContinuumCoulomb.ManufacturedEuler.inputRadiusProgram line 33
  9. opaque OAI.ContinuumCoulomb.ManufacturedEuler.boxProgram line 38
  10. opaque OAI.ContinuumCoulomb.ManufacturedEuler.stepProgram line 44
  11. opaque OAI.ContinuumCoulomb.ManufacturedEuler.environmentProgram line 48
  12. opaque OAI.ContinuumCoulomb.ManufacturedEuler.parameterNumbersProgram line 53
  13. opaque OAI.ContinuumCoulomb.ManufacturedEuler.parametersProgram line 57
  14. opaque OAI.ContinuumCoulomb.ManufacturedEuler.registersProgram line 62
  15. opaque OAI.ContinuumCoulomb.ManufacturedEuler.initialProgram line 67
  16. opaque OAI.ContinuumCoulomb.ManufacturedEuler.runArgumentsProgram line 74
  17. theorem OAI.ContinuumCoulomb.ManufacturedEuler.run_initial line 81
  18. opaque OAI.ContinuumCoulomb.ManufacturedEuler.program line 88
  19. def OAI.ContinuumCoulomb.ManufacturedEuler.certificate line 101