OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistorySamplerProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial generation of all sampled history packets. The runtime list is indexed by the unary number of source terms, not Hilbert-space dimension; each local matrix uses one of seven fixed arity programs.

  1. theorem OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.matrixData_instances line 18
  2. theorem OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.pair_matrixData_instances line 23
  3. abbrev OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.Input line 28
  4. def OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.inputCode line 29
  5. def OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.packet line 31
  6. def OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.entries line 36
  7. opaque OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.countProgram line 39
  8. opaque OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.packetProgram line 51
  9. opaque OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.program line 61
  10. theorem OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.packet_actual line 75
  11. theorem OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.entries_actual line 101
  12. def OAI.ContinuumCoulomb.QuantumHistorySamplerProgram.certificate line 109