OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDescriptorSiteProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial programs for the exact numeric support lists of every time-ordered rebit term and reference edge.

  1. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.oneLabel line 14
  2. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.consLabel line 19
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.distributedLabelsProgram line 25
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceWorkProgram line 52
  5. abbrev OAI.ContinuumCoulomb.QuantumHistoryDescriptors.ReferenceInput line 61
  6. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceCode line 62
  7. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.orderedAtProgram line 64
  8. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.rebitLabelsProgram line 70
  9. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.referenceLabelsProgram line 80
  10. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.supportLabelsProgram line 92
  11. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.supportCertificate line 95