OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateCode.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal constructors and coordinate selectors for the fixed H/T/CNOT alphabet used by the nearest-neighbor circuit preprocessor.

  1. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateTag line 12
  2. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateLeft line 17
  3. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateRight line 22
  4. def OAI.ContinuumCoulomb.QuantumCircuitCode.hadamardProgram line 27
  5. def OAI.ContinuumCoulomb.QuantumCircuitCode.phaseProgram line 31
  6. def OAI.ContinuumCoulomb.QuantumCircuitCode.cnotProgram line 35
  7. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateTagProgram line 40
  8. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateLeftProgram line 47
  9. def OAI.ContinuumCoulomb.QuantumCircuitCode.gateRightProgram line 52
  10. def OAI.ContinuumCoulomb.QuantumCircuitCode.swapList line 57
  11. theorem OAI.ContinuumCoulomb.QuantumCircuitCode.swapList_reverse line 60
  12. def OAI.ContinuumCoulomb.QuantumCircuitCode.swapListProgram line 62