OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumClockPath.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full literal clock path has bounded steps, including every row transition.

  1. theorem OAI.ContinuumCoulomb.qmaTaggedSweepFrom_head line 11
  2. theorem OAI.ContinuumCoulomb.qmaTaggedSweepFrom_chain line 22
  3. theorem OAI.ContinuumCoulomb.qmaSparseTags_chain line 60