OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistorySiteProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Literal ordered gate and propagation support lists. The values agree with the exact support order used by the local history matrix tables.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistorySiteProgram.GateInput line 16
  2. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.gateInputCode line 17
  3. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.gateLabels line 19
  4. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.gateLabelsProgram line 24
  5. theorem OAI.ContinuumCoulomb.QuantumHistorySiteProgram.gateLabels_actual line 41
  6. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.distributedNumber line 45
  7. abbrev OAI.ContinuumCoulomb.QuantumHistorySiteProgram.Input line 48
  8. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.inputCode line 49
  9. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.gateAt line 51
  10. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.propagationLabels line 53
  11. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.gateAtProgram line 57
  12. def OAI.ContinuumCoulomb.QuantumHistorySiteProgram.propagationLabelsProgram line 66
  13. theorem OAI.ContinuumCoulomb.QuantumHistorySiteProgram.propagationLabels_actual line 86