OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingInputProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Compile cell arrays and an edge array into the registers needed by the buffered-route evaluator. Binary endpoint labels are clipped by the explicit qubit array length before their conversion to unary loop bounds.

  1. abbrev OAI.ContinuumCoulomb.QuantumRoutingInputProgram.Data line 15
  2. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.dataCode line 16
  3. abbrev OAI.ContinuumCoulomb.QuantumRoutingInputProgram.Input line 18
  4. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.inputCode line 19
  5. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.edge line 21
  6. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.lane line 22
  7. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entry line 23
  8. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entries line 25
  9. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.fine line 28
  10. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.value line 31
  11. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.dataProgram line 39
  12. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.indexProgram line 40
  13. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.qubitsProgram line 41
  14. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.anchorsProgram line 44
  15. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.edgesProgram line 47
  16. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.edgeProgram line 50
  17. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.laneProgram line 54
  18. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.laneUnaryProgram line 56
  19. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entryProgram line 59
  20. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entriesProgram line 64
  21. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.program line 71
  22. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.pathProgram line 85