OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistorySpatialProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The literal sampled history and its row/column labels are combined into the exact prepared input of the fixed-round fork compiler.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.Input line 14
  2. abbrev OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.inputCode line 15
  3. def OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.sparseInput line 17
  4. opaque OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.sparseInputProgram line 19
  5. def OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.initialInput line 22
  6. opaque OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.initialInputProgram line 25
  7. def OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.prepared line 31
  8. opaque OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.cellsProgram line 34
  9. opaque OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.preparedProgram line 40
  10. theorem OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.rawCells_input line 49
  11. theorem OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.initialInput_actual line 64
  12. theorem OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.prepared_actual line 77
  13. def OAI.ContinuumCoulomb.QuantumHistorySpatialProgram.certificate line 85