OAI/MathematicalPhysics/ContinuumCoulomb/Programs/EulerVectorPrograms.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Rational vector arithmetic and bounded rounding for the three Euler registers. These are literal finite compositions of integer and rational stack programs.

  1. def OAI.ContinuumCoulomb.EulerRegisters.pointInputCode line 13
  2. def OAI.ContinuumCoulomb.EulerRegisters.proposalCode line 14
  3. def OAI.ContinuumCoulomb.EulerRegisters.roundInputCode line 15
  4. opaque OAI.ContinuumCoulomb.EulerRegisters.pointDenominatorProgram line 17
  5. opaque OAI.ContinuumCoulomb.EulerRegisters.pointRegistersProgram line 19
  6. opaque OAI.ContinuumCoulomb.EulerRegisters.firstRegisterProgram line 21
  7. opaque OAI.ContinuumCoulomb.EulerRegisters.tailRegisterProgram line 23
  8. opaque OAI.ContinuumCoulomb.EulerRegisters.secondRegisterProgram line 25
  9. opaque OAI.ContinuumCoulomb.EulerRegisters.thirdRegisterProgram line 27
  10. opaque OAI.ContinuumCoulomb.EulerRegisters.pointFirstProgram line 30
  11. opaque OAI.ContinuumCoulomb.EulerRegisters.pointSecondProgram line 33
  12. opaque OAI.ContinuumCoulomb.EulerRegisters.pointThirdProgram line 36
  13. opaque OAI.ContinuumCoulomb.EulerRegisters.pointProgram line 40
  14. opaque OAI.ContinuumCoulomb.EulerRegisters.tripleFirstProgram line 43
  15. opaque OAI.ContinuumCoulomb.EulerRegisters.tripleTailProgram line 45
  16. opaque OAI.ContinuumCoulomb.EulerRegisters.tripleSecondProgram line 47
  17. opaque OAI.ContinuumCoulomb.EulerRegisters.tripleThirdProgram line 49
  18. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalStepProgram line 52
  19. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalPairProgram line 54
  20. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalPointProgram line 56
  21. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalVelocityProgram line 58
  22. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalCoordinateProgram line 61
  23. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalProgram line 67
  24. opaque OAI.ContinuumCoulomb.EulerRegisters.roundParametersProgram line 72
  25. opaque OAI.ContinuumCoulomb.EulerRegisters.roundPointProgram line 74
  26. opaque OAI.ContinuumCoulomb.EulerRegisters.roundCoordinateProgram line 77
  27. opaque OAI.ContinuumCoulomb.EulerRegisters.roundProgram line 81