OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryBitProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Literal bit reads for the small history tables, and a bounded Boolean scan. The register bound is unary; this scan has no spin-configuration loop.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryBitProgram.Data line 13
  2. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.dataCode line 14
  3. abbrev OAI.ContinuumCoulomb.QuantumHistoryBitProgram.Query line 16
  4. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.queryCode line 17
  5. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.bit line 19
  6. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.row line 21
  7. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.column line 24
  8. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.readPair line 27
  9. opaque OAI.ContinuumCoulomb.QuantumHistoryBitProgram.rowProgram line 29
  10. opaque OAI.ContinuumCoulomb.QuantumHistoryBitProgram.columnProgram line 41
  11. opaque OAI.ContinuumCoulomb.QuantumHistoryBitProgram.readPairProgram line 54
  12. theorem OAI.ContinuumCoulomb.QuantumHistoryBitProgram.bit_as_test line 58
  13. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.matrixEntry line 66
  14. opaque OAI.ContinuumCoulomb.QuantumHistoryBitProgram.matrixEntryProgram line 69
  15. def OAI.ContinuumCoulomb.QuantumHistoryBitProgram.allBits line 83
  16. theorem OAI.ContinuumCoulomb.QuantumHistoryBitProgram.fold_and line 85
  17. opaque OAI.ContinuumCoulomb.QuantumHistoryBitProgram.allProgram line 93
  18. theorem OAI.ContinuumCoulomb.QuantumHistoryBitProgram.row_actual line 102
  19. theorem OAI.ContinuumCoulomb.QuantumHistoryBitProgram.column_actual line 114