OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/EulerRegisters.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Three bounded integer numerator registers suffice for a rounded Euler trajectory. The size invariant is unconditional on the supplied sampler; it therefore supports polynomial-time iteration on every encoded input.

  1. abbrev OAI.ContinuumCoulomb.EulerRegisters.Registers line 15
  2. abbrev OAI.ContinuumCoulomb.EulerRegisters.Parameters line 16
  3. abbrev OAI.ContinuumCoulomb.EulerRegisters.Config line 17
  4. def OAI.ContinuumCoulomb.EulerRegisters.registersCode line 19
  5. def OAI.ContinuumCoulomb.EulerRegisters.parametersCode line 20
  6. def OAI.ContinuumCoulomb.EulerRegisters.configCode line 22
  7. def OAI.ContinuumCoulomb.EulerRegisters.point line 25
  8. def OAI.ContinuumCoulomb.EulerRegisters.round line 28
  9. def OAI.ContinuumCoulomb.EulerRegisters.proposal line 32
  10. def OAI.ContinuumCoulomb.EulerRegisters.advance line 35
  11. theorem OAI.ContinuumCoulomb.EulerRegisters.parameters_length line 41
  12. theorem OAI.ContinuumCoulomb.EulerRegisters.config_length line 47
  13. theorem OAI.ContinuumCoulomb.EulerRegisters.iterate_parameters line 55
  14. theorem OAI.ContinuumCoulomb.EulerRegisters.iterate_counter line 61
  15. theorem OAI.ContinuumCoulomb.EulerRegisters.iterate_register_bounds line 71
  16. theorem OAI.ContinuumCoulomb.EulerRegisters.iterate_code_bound line 84