OAI/Computability/QuantumFactoring/CircuitProgramEmission.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.data line 16
  2. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.count line 20
  3. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.outLength line 24
  4. def OAI.ExactQuantumFactoring.CircuitEmission.oracleOnOps line 33
  5. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_oracleOn line 35
  6. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_firstProgram line 45
  7. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_reverseProgram line 52
  8. def OAI.ExactQuantumFactoring.CircuitEmission.phaseOp line 57
  9. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_phaseAt line 58
  10. def OAI.ExactQuantumFactoring.CircuitEmission.phaseOps line 60
  11. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_phaseOracle line 62
  12. def OAI.ExactQuantumFactoring.CircuitEmission.amplifyOps line 67
  13. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_amplification line 69
  14. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.oracleIndexP line 77
  15. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.oracleOnOpsP line 90
  16. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.phaseOpP line 94
  17. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.phaseOpsP line 97
  18. abbrev OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits line 103
  19. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.congr line 107
  20. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.append line 109
  21. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.first line 112
  22. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.reverse line 114
  23. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.oracleOn line 117
  24. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.phase line 120
  25. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.amplify line 123
  26. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.readout line 129