OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListScheduleProgram.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

A fixed-round routing compiler on literal bond/work lists. Each active edge receives one singlet pair; its unfinished tail retains one less work unit.

  1. abbrev OAI.ContinuumCoulomb.QuantumListSchedule.Entry line 12
  2. def OAI.ContinuumCoulomb.QuantumListSchedule.entryCode line 13
  3. def OAI.ContinuumCoulomb.QuantumListSchedule.zeroEntry line 14
  4. def OAI.ContinuumCoulomb.QuantumListSchedule.selected line 15
  5. def OAI.ContinuumCoulomb.QuantumListSchedule.partition line 16
  6. def OAI.ContinuumCoulomb.QuantumListSchedule.erase line 17
  7. opaque OAI.ContinuumCoulomb.QuantumListSchedule.selectedProgram line 19
  8. opaque OAI.ContinuumCoulomb.QuantumListSchedule.partitionProgram line 25
  9. opaque OAI.ContinuumCoulomb.QuantumListSchedule.eraseProgram line 41
  10. abbrev OAI.ContinuumCoulomb.QuantumListSchedule.State line 44
  11. def OAI.ContinuumCoulomb.QuantumListSchedule.stateCode line 45
  12. abbrev OAI.ContinuumCoulomb.QuantumListSchedule.Input line 46
  13. def OAI.ContinuumCoulomb.QuantumListSchedule.inputCode line 47
  14. def OAI.ContinuumCoulomb.QuantumListSchedule.stepInput line 49
  15. opaque OAI.ContinuumCoulomb.QuantumListSchedule.stateProgram line 52
  16. opaque OAI.ContinuumCoulomb.QuantumListSchedule.precisionProgram line 53
  17. opaque OAI.ContinuumCoulomb.QuantumListSchedule.countInputProgram line 54
  18. opaque OAI.ContinuumCoulomb.QuantumListSchedule.tailProgram line 56
  19. opaque OAI.ContinuumCoulomb.QuantumListSchedule.scalarInputProgram line 58
  20. opaque OAI.ContinuumCoulomb.QuantumListSchedule.entriesProgram line 60
  21. opaque OAI.ContinuumCoulomb.QuantumListSchedule.selectedEntriesProgram line 62
  22. opaque OAI.ContinuumCoulomb.QuantumListSchedule.stepInputProgram line 65
  23. abbrev OAI.ContinuumCoulomb.QuantumListSchedule.BlockInput line 72
  24. def OAI.ContinuumCoulomb.QuantumListSchedule.blockInputCode line 73
  25. def OAI.ContinuumCoulomb.QuantumListSchedule.blockBondInput line 75
  26. def OAI.ContinuumCoulomb.QuantumListSchedule.blockWork line 76
  27. def OAI.ContinuumCoulomb.QuantumListSchedule.block line 77
  28. opaque OAI.ContinuumCoulomb.QuantumListSchedule.blockBondInputProgram line 80
  29. opaque OAI.ContinuumCoulomb.QuantumListSchedule.blockWorkProgram line 88
  30. opaque OAI.ContinuumCoulomb.QuantumListSchedule.blockProgram line 99
  31. def OAI.ContinuumCoulomb.QuantumListSchedule.indexed line 104
  32. def OAI.ContinuumCoulomb.QuantumListSchedule.family line 107
  33. def OAI.ContinuumCoulomb.QuantumListSchedule.value line 110
  34. opaque OAI.ContinuumCoulomb.QuantumListSchedule.indexedProgram line 114
  35. opaque OAI.ContinuumCoulomb.QuantumListSchedule.familyLengthProgram line 123
  36. opaque OAI.ContinuumCoulomb.QuantumListSchedule.familyTabProgram line 128
  37. opaque OAI.ContinuumCoulomb.QuantumListSchedule.familyInputProgram line 133
  38. opaque OAI.ContinuumCoulomb.QuantumListSchedule.familyNestedProgram line 137
  39. opaque OAI.ContinuumCoulomb.QuantumListSchedule.familyProgram line 141
  40. opaque OAI.ContinuumCoulomb.QuantumListSchedule.program line 144
  41. def OAI.ContinuumCoulomb.QuantumListSchedule.iterate line 150
  42. opaque OAI.ContinuumCoulomb.QuantumListSchedule.iterateProgram line 154