OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFirstUseProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Literal first-use indices for the actual circuit gates. The fold stores a unary index bounded by the gate-list length, including the no-use case.

  1. abbrev OAI.ContinuumCoulomb.QuantumFirstUseProgram.TouchInput line 17
  2. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.touchCode line 18
  3. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.touches line 21
  4. theorem OAI.ContinuumCoulomb.QuantumFirstUseProgram.touches_spec line 25
  5. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.touchesProgram line 38
  6. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.step line 50
  7. theorem OAI.ContinuumCoulomb.QuantumFirstUseProgram.step_le line 52
  8. theorem OAI.ContinuumCoulomb.QuantumFirstUseProgram.fold_le line 55
  9. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.first line 65
  10. theorem OAI.ContinuumCoulomb.QuantumFirstUseProgram.first_eq_findIdx line 67
  11. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.stepProgram line 73
  12. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.foldProgram line 80
  13. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.firstProgram line 91
  14. abbrev OAI.ContinuumCoulomb.QuantumFirstUseProgram.Input line 98
  15. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.inputCode line 99
  16. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.touchList line 101
  17. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.value line 104
  18. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.touchListProgram line 106
  19. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.program line 122
  20. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.certificate line 125
  21. theorem OAI.ContinuumCoulomb.QuantumFirstUseProgram.value_eq line 128
  22. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.allValues line 138
  23. def OAI.ContinuumCoulomb.QuantumFirstUseProgram.allProgram line 141
  24. theorem OAI.ContinuumCoulomb.QuantumFirstUseProgram.allValues_eq line 149