OAI/MathematicalPhysics/ContinuumCoulomb/Programs/EulerProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The bounded-register Euler loop is an actual polynomial-time TM2 program whenever its field sampler is one. The size invariant was proved for arbitrary sampler outputs, so this certificate holds on all inputs.

  1. opaque OAI.ContinuumCoulomb.EulerRegisters.parametersProgram line 15
  2. opaque OAI.ContinuumCoulomb.EulerRegisters.environmentProgram line 17
  3. opaque OAI.ContinuumCoulomb.EulerRegisters.parameterTailProgram line 19
  4. opaque OAI.ContinuumCoulomb.EulerRegisters.denominatorProgram line 22
  5. opaque OAI.ContinuumCoulomb.EulerRegisters.boxStepProgram line 24
  6. opaque OAI.ContinuumCoulomb.EulerRegisters.boxProgram line 26
  7. opaque OAI.ContinuumCoulomb.EulerRegisters.stepProgram line 28
  8. opaque OAI.ContinuumCoulomb.EulerRegisters.stateProgram line 30
  9. opaque OAI.ContinuumCoulomb.EulerRegisters.counterProgram line 32
  10. opaque OAI.ContinuumCoulomb.EulerRegisters.registersProgram line 34
  11. opaque OAI.ContinuumCoulomb.EulerRegisters.currentPointProgram line 37
  12. opaque OAI.ContinuumCoulomb.EulerRegisters.timeProgram line 41
  13. opaque OAI.ContinuumCoulomb.EulerRegisters.sampleArgumentsProgram line 45
  14. opaque OAI.ContinuumCoulomb.EulerRegisters.velocityProgram line 52
  15. opaque OAI.ContinuumCoulomb.EulerRegisters.proposalArgumentsProgram line 59
  16. opaque OAI.ContinuumCoulomb.EulerRegisters.nextPointProgram line 66
  17. opaque OAI.ContinuumCoulomb.EulerRegisters.nextRegistersProgram line 74
  18. opaque OAI.ContinuumCoulomb.EulerRegisters.advanceProgram line 82
  19. opaque OAI.ContinuumCoulomb.EulerRegisters.repeatProgram line 89
  20. def OAI.ContinuumCoulomb.EulerRegisters.run line 97
  21. opaque OAI.ContinuumCoulomb.EulerRegisters.program line 101
  22. def OAI.ContinuumCoulomb.EulerRegisters.certificate line 107