OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumClockStep.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Each active guarded clock pair is either entirely legal or entirely illegal; its legal pair is the intended consecutive history pair.

  1. theorem OAI.ContinuumCoulomb.qmaClock_step_guard line 12
  2. theorem OAI.ContinuumCoulomb.qmaClock_step_zero line 18
  3. theorem OAI.ContinuumCoulomb.qmaClock_step_update line 22
  4. theorem OAI.ContinuumCoulomb.qmaClock_step_legal_iff line 34
  5. theorem OAI.ContinuumCoulomb.qmaClock_step_legal_before line 47