OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPreparedCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The particular sparse, nonempty circuit used by the history reduction, with its literal program and unchanged verifier acceptance probability.

  1. def OAI.ContinuumCoulomb.qmaPreparedCircuit line 13
  2. theorem OAI.ContinuumCoulomb.qmaPreparedCircuit_witness line 16
  3. theorem OAI.ContinuumCoulomb.qmaPreparedCircuit_wellFormed line 19
  4. theorem OAI.ContinuumCoulomb.qmaPreparedCircuit_positive line 23
  5. theorem OAI.ContinuumCoulomb.qmaPreparedCircuit_acceptance line 26
  6. theorem OAI.ContinuumCoulomb.qmaPreparedCircuit_size line 34
  7. def OAI.ContinuumCoulomb.QuantumCircuitCode.preparedCircuitProgram line 50
  8. def OAI.ContinuumCoulomb.QuantumVerifier.prepared line 55
  9. theorem OAI.ContinuumCoulomb.QuantumVerifier.prepared_wellFormed line 58
  10. theorem OAI.ContinuumCoulomb.QuantumVerifier.prepared_positive line 61
  11. def OAI.ContinuumCoulomb.QuantumVerifier.preparedSize line 64
  12. theorem OAI.ContinuumCoulomb.QuantumVerifier.prepared_size line 67