OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalBoxRound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Bounded integer numerator registers for rounded Euler iteration. Clipping to a fixed box prevents malformed evaluator outputs from causing unbounded register growth. On valid trajectories clipping never increases the distance to the exact coordinate.

  1. def OAI.ContinuumCoulomb.RationalBoxRound.clip line 15
  2. theorem OAI.ContinuumCoulomb.RationalBoxRound.clip_bounds line 17
  3. theorem OAI.ContinuumCoulomb.RationalBoxRound.clip_natAbs line 22
  4. def OAI.ContinuumCoulomb.RationalBoxRound.numerator line 28
  5. def OAI.ContinuumCoulomb.RationalBoxRound.value line 29
  6. theorem OAI.ContinuumCoulomb.RationalBoxRound.numerator_bits line 31
  7. theorem OAI.ContinuumCoulomb.RationalBoxRound.clip_real_error line 35
  8. theorem OAI.ContinuumCoulomb.RationalBoxRound.value_error line 49
  9. abbrev OAI.ContinuumCoulomb.RationalBoxRound.Input line 81
  10. def OAI.ContinuumCoulomb.RationalBoxRound.inputCode line 82
  11. opaque OAI.ContinuumCoulomb.RationalBoxRound.clipProgram line 84
  12. opaque OAI.ContinuumCoulomb.RationalBoxRound.numeratorProgram line 100
  13. opaque OAI.ContinuumCoulomb.RationalBoxRound.program line 109
  14. def OAI.ContinuumCoulomb.RationalBoxRound.certificate line 116