OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryDescriptorProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomial generation of the literal history-term descriptor list. Only the circuit's unary work count and gate-list length control enumeration.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryDescriptors.IndexInput line 12
  2. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.indexCode line 13
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.atIndexProgram line 16
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.timeProgram line 42
  5. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.countProgram line 47
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.sourceEntryProgram line 55
  7. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.sourceProgram line 64
  8. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.sourceCertificate line 69