OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedRawPackingProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

A literal polynomial program for the final ordered X/Z classifier. It reads two site-label pairs and never enumerates a spin basis.

  1. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.letterCode line 13
  2. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.inputCode line 14
  3. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.entry line 15
  4. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.weightProgram line 17
  5. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.entriesProgram line 18
  6. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.entryProgram line 20
  7. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.indexProgram line 23
  8. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.labelProgram line 25
  9. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.labelTest line 27
  10. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.lengthProgram line 30
  11. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.lengthTest line 33
  12. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.sameIndexProgram line 36
  13. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.scalarProgram line 40
  14. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.nonzeroFieldProgram line 47
  15. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.fieldProgram line 55
  16. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.pairProgram line 61
  17. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.lookupValue line 67
  18. theorem OAI.ContinuumCoulomb.QuantumOrderedRawPacking.lookupValue_eq line 75
  19. opaque OAI.ContinuumCoulomb.QuantumOrderedRawPacking.program line 84
  20. def OAI.ContinuumCoulomb.QuantumOrderedRawPacking.certificate line 94