OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryPenalty.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The adjacent 01 penalties separate all invalid unary clock states.

  1. def OAI.ContinuumCoulomb.qmaClockFaultCount line 11
  2. theorem OAI.ContinuumCoulomb.qmaClockFaultCount_nonneg line 15
  3. theorem OAI.ContinuumCoulomb.qmaClockFaultCount_zero line 21
  4. theorem OAI.ContinuumCoulomb.qmaClockFaultCount_one_le line 35
  5. theorem OAI.ContinuumCoulomb.qmaClockFaultCount_unary line 60
  6. theorem OAI.ContinuumCoulomb.qmaClockFaultCount_invalid line 64