OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelCompile.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The literal six-local sparse-word compiler followed by the rational four-spin compiler. Its only input is a precision, a unary qubit count, and the ordered rational sparse-word list.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.Input line 16
  2. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.qubitCount line 18
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.classify line 20
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.labelEntries line 23
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.rawEntries line 25
  6. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.outputCount line 27
  7. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.rawInput line 29
  8. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.output line 32
  9. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.classifyProgram line 35
  10. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.labelEntriesProgram line 40
  11. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.rawEntriesProgram line 45
  12. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.outputCountProgram line 49
  13. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.outputProgram line 52
  14. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.certificate line 59
  15. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.finalSites line 65
  16. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.finalWord line 68
  17. def OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.finalCoefficient line 71
  18. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.output_table line 74
  19. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.qubitCount_table line 89