OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListScheduleGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The exact emitted edge order realizes the abstract scheduled subdivision. This transfers the disjoint-route invariant to the literal list compiler.

  1. def OAI.ContinuumCoulomb.QuantumListSchedule.role line 14
  2. def OAI.ContinuumCoulomb.QuantumListSchedule.unrole line 18
  3. def OAI.ContinuumCoulomb.QuantumListSchedule.roleEquiv line 23
  4. theorem OAI.ContinuumCoulomb.QuantumListSchedule.oldValue line 35
  5. theorem OAI.ContinuumCoulomb.QuantumListSchedule.freshValue line 36
  6. def OAI.ContinuumCoulomb.QuantumListSchedule.nextEdge line 41
  7. theorem OAI.ContinuumCoulomb.QuantumListSchedule.value_count line 47
  8. def OAI.ContinuumCoulomb.QuantumListSchedule.nextVertex line 51
  9. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indexed_entry line 56
  10. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indexed_bond line 62
  11. def OAI.ContinuumCoulomb.QuantumListSchedule.tagLeft line 68
  12. def OAI.ContinuumCoulomb.QuantumListSchedule.tagRight line 75
  13. theorem OAI.ContinuumCoulomb.QuantumListSchedule.left_tag line 80
  14. theorem OAI.ContinuumCoulomb.QuantumListSchedule.right_tag line 98
  15. def OAI.ContinuumCoulomb.QuantumListSchedule.tagEdge line 114
  16. theorem OAI.ContinuumCoulomb.QuantumListSchedule.nextEdge_eq line 119
  17. theorem OAI.ContinuumCoulomb.QuantumListSchedule.nextEdge_tag line 126
  18. theorem OAI.ContinuumCoulomb.QuantumListSchedule.tag_left_relabel line 131
  19. theorem OAI.ContinuumCoulomb.QuantumListSchedule.tag_right_relabel line 141
  20. theorem OAI.ContinuumCoulomb.QuantumListSchedule.work_tag line 151
  21. theorem OAI.ContinuumCoulomb.QuantumListSchedule.next_left line 163
  22. theorem OAI.ContinuumCoulomb.QuantumListSchedule.next_right line 172
  23. theorem OAI.ContinuumCoulomb.QuantumListSchedule.next_work line 181
  24. def OAI.ContinuumCoulomb.QuantumListSchedule.nextRelabel line 188