OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryPreparedProgram.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The nonempty circuit, final unary precision, exact history cells and rational promise thresholds are assembled without semantic input oracles.

  1. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.precision line 13
  2. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.time line 16
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.timeProgram line 18
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.precisionProgram line 21
  5. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.scheduled line 28
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.scheduledProgram line 31
  7. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.prepared line 35
  8. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.preparedProgram line 38
  9. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.grid line 42
  10. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.gridProgram line 45
  11. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.routing line 49
  12. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.routingProgram line 52
  13. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.thresholds line 56
  14. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.thresholdTimeProgram line 60
  15. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.lowerProgram line 65
  16. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.upperProgram line 75
  17. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.thresholdsProgram line 85
  18. abbrev OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.FinalInput line 89
  19. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.finalInputCode line 90
  20. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.finalInput line 93
  21. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.rationalPrecisionProgram line 96
  22. opaque OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.finalInputProgram line 100
  23. theorem OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.precision_pos line 103
  24. theorem OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.thresholds_lt line 106
  25. theorem OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.thresholds_gap line 109
  26. theorem OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.prepared_actual line 113
  27. theorem OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.routing_actual line 120
  28. theorem OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.finalInput_actual line 128
  29. def OAI.ContinuumCoulomb.QuantumHistoryPreparedProgram.certificate line 138