OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumNearestProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal nearest-neighbor gate compilation. All finite loops use the unary work bound; malformed gate indices take the original singleton branch.

  1. abbrev OAI.ContinuumCoulomb.QuantumCircuitCode.NearestInput line 12
  2. def OAI.ContinuumCoulomb.QuantumCircuitCode.nearestInputCode line 13
  3. def OAI.ContinuumCoulomb.QuantumCircuitCode.forwardGuard line 15
  4. def OAI.ContinuumCoulomb.QuantumCircuitCode.backwardGuard line 17
  5. def OAI.ContinuumCoulomb.QuantumCircuitCode.nearestValue line 20
  6. theorem OAI.ContinuumCoulomb.QuantumCircuitCode.nearestValue_eq line 29
  7. def OAI.ContinuumCoulomb.QuantumCircuitCode.workBits line 64
  8. def OAI.ContinuumCoulomb.QuantumCircuitCode.leftBits line 66
  9. def OAI.ContinuumCoulomb.QuantumCircuitCode.rightBits line 68
  10. def OAI.ContinuumCoulomb.QuantumCircuitCode.forwardGuardProgram line 71
  11. def OAI.ContinuumCoulomb.QuantumCircuitCode.backwardGuardProgram line 78
  12. def OAI.ContinuumCoulomb.QuantumCircuitCode.nearestProgram line 85
  13. def OAI.ContinuumCoulomb.QuantumCircuitCode.nearestListProgram line 108
  14. def OAI.ContinuumCoulomb.QuantumCircuitCode.nearestCircuitProgram line 121