OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalRealification.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The realification uses one shared extra qubit and adds at most one qubit to each interaction support.

  1. def OAI.ContinuumCoulomb.qmaRebitSites line 15
  2. def OAI.ContinuumCoulomb.qmaRebitOnQubits line 18
  3. theorem OAI.ContinuumCoulomb.qmaRebitSites_card line 23
  4. theorem OAI.ContinuumCoulomb.qmaRebitOnQubits_local line 26
  5. theorem OAI.ContinuumCoulomb.qmaRebitOnQubits_add line 67
  6. theorem OAI.ContinuumCoulomb.qmaRebitOnQubits_smul line 74