OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateEntryProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Exact gate entries from a bounded register scan. Work is unary, addresses and support labels are binary, and each quantum bit is read from the supplied small support table. No sum over ambient configurations occurs.

  1. abbrev OAI.ContinuumCoulomb.QuantumGateEntryProgram.Input line 15
  2. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.inputCode line 16
  3. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.left line 19
  4. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.right line 20
  5. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.row line 21
  6. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.column line 22
  7. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.point line 24
  8. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.allWork line 31
  9. theorem OAI.ContinuumCoulomb.QuantumGateEntryProgram.allWork_iff line 33
  10. theorem OAI.ContinuumCoulomb.QuantumGateEntryProgram.allWork_single line 38
  11. theorem OAI.ContinuumCoulomb.QuantumGateEntryProgram.swap_val line 53
  12. theorem OAI.ContinuumCoulomb.QuantumGateEntryProgram.allWork_cnot line 56
  13. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.entry line 90
  14. theorem OAI.ContinuumCoulomb.QuantumGateEntryProgram.entry_eq line 99
  15. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.leftProgram line 147
  16. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.rightProgram line 159
  17. abbrev OAI.ContinuumCoulomb.QuantumGateEntryProgram.PointInput line 171
  18. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.pointCode line 172
  19. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.queryProgram line 174
  20. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.pointRowProgram line 187
  21. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.pointColumnProgram line 190
  22. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.tagProgram line 193
  23. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.pointProgram line 201
  24. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.allWorkProgram line 224
  25. opaque OAI.ContinuumCoulomb.QuantumGateEntryProgram.entryProgram line 236
  26. def OAI.ContinuumCoulomb.QuantumGateEntryProgram.certificate line 258
  27. theorem OAI.ContinuumCoulomb.QuantumGateEntryProgram.entry_on_support line 261