OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryDelta.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact register evaluation of the propagation delta. The equality scans are bounded by the unary circuit size; every bit is read from the supplied local support table.

  1. def OAI.ContinuumCoulomb.QuantumHistoryDelta.guard line 16
  2. def OAI.ContinuumCoulomb.QuantumHistoryDelta.flipped line 19
  3. def OAI.ContinuumCoulomb.QuantumHistoryDelta.sameClock line 23
  4. def OAI.ContinuumCoulomb.QuantumHistoryDelta.entry line 26
  5. def OAI.ContinuumCoulomb.QuantumHistoryDelta.qubitEquiv line 34
  6. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.qubitEquiv_val line 37
  7. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.readRow_eq line 41
  8. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.readColumn_eq line 46
  9. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.guard_iff line 51
  10. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.flipped_iff line 63
  11. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.sameClock_iff line 73
  12. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.gate_entry line 80
  13. theorem OAI.ContinuumCoulomb.QuantumHistoryDelta.entry_actual line 88