OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalPropagation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Every guarded propagation term acts on three clock bits and at most two computation bits. This is the actual unary-clock operator.

  1. abbrev OAI.ContinuumCoulomb.QMACircuitQubit line 13
  2. def OAI.ContinuumCoulomb.qmaCircuitQubitSplit line 15
  3. def OAI.ContinuumCoulomb.qmaPropagationSites line 19
  4. theorem OAI.ContinuumCoulomb.qmaPropagationSites_card line 24
  5. def OAI.ContinuumCoulomb.qmaGuardProjection line 43
  6. def OAI.ContinuumCoulomb.qmaLocalPropagationDelta line 48
  7. theorem OAI.ContinuumCoulomb.qmaGuardProjection_local line 54
  8. theorem OAI.ContinuumCoulomb.qmaLocalPropagationDelta_local line 66
  9. theorem OAI.ContinuumCoulomb.qmaLocalPropagationGram_local line 78