OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorAncilla.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Occupation coordinates for the parallel qubit mediator gadgets.

  1. def OAI.ContinuumCoulomb.qmaAncillaVacuum line 14
  2. def OAI.ContinuumCoulomb.qmaAncillaSingle line 16
  3. theorem OAI.ContinuumCoulomb.qmaAncillaSingle_apply line 19
  4. theorem OAI.ContinuumCoulomb.qmaAncillaSingle_ne_vacuum line 24
  5. theorem OAI.ContinuumCoulomb.qmaAncillaSingle_injective line 30
  6. theorem OAI.ContinuumCoulomb.qmaBitFlip_vacuum line 37
  7. theorem OAI.ContinuumCoulomb.qmaBitFlip_single_self line 41
  8. theorem OAI.ContinuumCoulomb.qmaBitFlip_single_ne_single line 45
  9. def OAI.ContinuumCoulomb.qmaAncillaNumber line 59
  10. theorem OAI.ContinuumCoulomb.qmaAncillaNumber_vacuum line 62
  11. theorem OAI.ContinuumCoulomb.qmaAncillaNumber_single line 66
  12. theorem OAI.ContinuumCoulomb.qmaAncillaNumber_pos line 71
  13. def OAI.ContinuumCoulomb.qmaAncillaOccupation line 83
  14. theorem OAI.ContinuumCoulomb.qmaAncillaOccupation_single line 86
  15. theorem OAI.ContinuumCoulomb.qmaBitFlipMatrix_single line 97
  16. theorem OAI.ContinuumCoulomb.qmaBitFlipMatrix_vacuum_right line 101
  17. theorem OAI.ContinuumCoulomb.qmaAncillaOccupation_vacuum_right line 106