OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUntouchedInput.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A qubit's initialization check can be placed immediately before its first gate.

  1. theorem OAI.ContinuumCoulomb.QMALocalOn.entry_zero_of_outside line 13
  2. theorem OAI.ContinuumCoulomb.qmaLocal_mask_commute line 24
  3. theorem OAI.ContinuumCoulomb.qmaGateProduct_mask_commute line 50
  4. theorem OAI.ContinuumCoulomb.qmaInputCheck_prefix_untouched line 62
  5. theorem OAI.ContinuumCoulomb.qmaDistributedHistoryEnergy_sound_untouched line 74