OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathRelabelingNext.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Relabeling commutes with a scheduled subdivision. This identifies the literal list order with the physical port graph through every round.

  1. def OAI.ContinuumCoulomb.QMAPathRelabeling.activeEquiv line 14
  2. def OAI.ContinuumCoulomb.QMAPathRelabeling.retainedEquiv line 16
  3. def OAI.ContinuumCoulomb.QMAPathRelabeling.activeIndex line 18
  4. theorem OAI.ContinuumCoulomb.QMAPathRelabeling.selected_index line 21
  5. def OAI.ContinuumCoulomb.QMAPathRelabeling.nextVertex line 26
  6. def OAI.ContinuumCoulomb.QMAPathRelabeling.nextEdge line 29
  7. theorem OAI.ContinuumCoulomb.QMAPathRelabeling.nextVertex_old line 33
  8. theorem OAI.ContinuumCoulomb.QMAPathRelabeling.nextVertex_fresh line 35
  9. theorem OAI.ContinuumCoulomb.QMAPathRelabeling.next_left line 39
  10. theorem OAI.ContinuumCoulomb.QMAPathRelabeling.next_right line 53
  11. theorem OAI.ContinuumCoulomb.QMAPathRelabeling.next_work line 63
  12. def OAI.ContinuumCoulomb.QMAPathRelabeling.next line 72