OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortSchedulePacking.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual computed scheduler begins with the exact spatial exchange graph, with one work counter for each of its enumerated interactions.

  1. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.port_layout line 13
  2. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.bounded_of_lists line 28
  3. theorem OAI.ContinuumCoulomb.QuantumPortSchedulePacking.state_eq line 54
  4. theorem OAI.ContinuumCoulomb.QuantumPortSchedulePacking.valid line 68
  5. theorem OAI.ContinuumCoulomb.QuantumPortSchedulePacking.energy line 74
  6. theorem OAI.ContinuumCoulomb.QuantumPortSchedulePacking.layout_eq line 80
  7. theorem OAI.ContinuumCoulomb.QuantumPortSchedulePacking.has_representation line 92