OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryRawCells.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The computed cell array has the exact physical-spin order of the raw history compiler, including all six mediator layers and the four-spin blocks.

  1. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.map_cell6 line 16
  2. def OAI.ContinuumCoulomb.QuantumHistoryCells.rawCells line 31
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryCells.rawCellsProgram line 33
  4. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.rawCells_actual line 37
  5. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.rawCells_length line 59
  6. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.rawCells_get line 68
  7. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.input_cell line 77
  8. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.rawCells_input_length line 86
  9. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.rawCells_input_get line 93
  10. def OAI.ContinuumCoulomb.QuantumHistoryCells.rawCertificate line 101