OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelOutput.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The complete literal sparse-label compiler equals the actual ordered six-to-four-to-three-to-two-to-XZ construction and private-pair stage.

  1. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.terms1 line 14
  2. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.terms2 line 15
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.terms3 line 16
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.terms4 line 17
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.terms5 line 18
  6. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.terms6 line 19
  7. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.qubits1 line 21
  8. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.qubits2 line 22
  9. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.qubits3 line 23
  10. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.qubits4 line 24
  11. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.qubits5 line 25
  12. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.qubits6 line 26
  13. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.finalCount line 28
  14. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.finalCount_eq line 31
  15. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.output_table line 37