OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumClockTransition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A guarded single-bit clock update preserves the legal clock sector. The guard inspects only the two adjacent clock bits.

  1. def OAI.ContinuumCoulomb.qmaClockLeft line 11
  2. def OAI.ContinuumCoulomb.qmaClockMiddle line 12
  3. def OAI.ContinuumCoulomb.qmaClockRight line 13
  4. def OAI.ContinuumCoulomb.QMAClockGuard line 15
  5. theorem OAI.ContinuumCoulomb.qmaClockLeft_ne_middle line 18
  6. theorem OAI.ContinuumCoulomb.qmaClockRight_ne_middle line 25
  7. theorem OAI.ContinuumCoulomb.qmaClockGuard_update line 32
  8. theorem OAI.ContinuumCoulomb.qmaClock_update_antitone line 37
  9. theorem OAI.ContinuumCoulomb.qmaClock_update_legal line 65