OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryDiagonalProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar-register evaluation of the diagonal history descriptors.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryDiagonal.Input line 13
  2. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.inputCode line 14
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.circuitProgram line 16
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.descriptorProgram line 17
  5. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.dataProgram line 19
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tagProgram line 21
  7. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.indexProgram line 23
  8. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.timeProgram line 25
  9. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.clockBaseProgram line 28
  10. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.workBaseProgram line 32
  11. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.clockValueProgram line 37
  12. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.workValueProgram line 41
  13. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.firstUseProgram line 45
  14. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.weightProgram line 50
  15. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.weightCertificate line 88