OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelPipeline.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A fixed six-stage literal sparse-word compiler. The final stage assigns a private mediator to every two-local term before the four-spin encoding.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.Input line 14
  2. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.State line 15
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.fourWeight line 17
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.sevenWeight line 18
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.subdivisionStep line 20
  6. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.thirdStep line 22
  7. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.yyStep line 23
  8. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.privateStep line 24
  9. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.output line 25
  10. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.subdivisionStepProgram line 28
  11. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.thirdStepProgram line 32
  12. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.yyStepProgram line 35
  13. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.privateStepProgram line 38
  14. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.outputProgram line 41
  15. def OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.certificate line 46
  16. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.output_length line 49
  17. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelPipeline.output_qubits line 53