OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistorySourceProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The complete literal circuit-to-source map, including nonempty padding, sampling precision, fork and route programs, and rational thresholds.

  1. def OAI.ContinuumCoulomb.QuantumHistorySourceProgram.value line 14
  2. theorem OAI.ContinuumCoulomb.QuantumHistorySourceProgram.inputCode_eq line 18
  3. opaque OAI.ContinuumCoulomb.QuantumHistorySourceProgram.inputProgram line 21
  4. opaque OAI.ContinuumCoulomb.QuantumHistorySourceProgram.program line 26
  5. theorem OAI.ContinuumCoulomb.QuantumHistorySourceProgram.value_actual line 35
  6. def OAI.ContinuumCoulomb.QuantumHistorySourceProgram.certificate line 47
  7. def OAI.ContinuumCoulomb.QuantumHistorySourceProgram.fromVerifier line 50
  8. def OAI.ContinuumCoulomb.QuantumHistorySourceProgram.fromVerifier_uniform line 52
  9. theorem OAI.ContinuumCoulomb.QuantumHistorySourceProgram.fromVerifier_actual line 57