OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedPacketProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Polynomial postprocessing of the actual fixed-size local matrix payloads. This emits the full raw exchange list and its scalar offset.

  1. abbrev OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.Payload line 13
  2. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.payloadCode line 14
  3. abbrev OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.FamilyInput line 15
  4. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.familyCode line 16
  5. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.family line 18
  6. opaque OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.familyProgram line 21
  7. abbrev OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.Input line 29
  8. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.inputCode line 30
  9. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.prepare line 33
  10. opaque OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.prepareProgram line 36
  11. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.output line 44
  12. opaque OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.outputProgram line 46
  13. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.certificate line 50
  14. def OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.sourcePayloads line 58
  15. theorem OAI.ContinuumCoulomb.QuantumPaddedPacketProgram.family_source line 63