OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPackedSchedule.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Packing a finite exchange graph with a work counter retains its endpoints and work exactly. This bridges the literal schedule to the geometric one.

  1. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.schedule_congr line 14
  2. def OAI.ContinuumCoulomb.QuantumPackedSchedule.state line 19
  3. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.erase_state line 24
  4. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.valid line 28
  5. def OAI.ContinuumCoulomb.QuantumPackedSchedule.scheduleRelabel line 36
  6. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.energy line 59
  7. def OAI.ContinuumCoulomb.QuantumPackedSchedule.layout line 65
  8. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.layout_represents line 71
  9. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.layout_has_representation line 88