OAI/Combinatorics/UniformKServer/HeavyProcessEdits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

End-to-end heavy edits and physical movement, including all no-insertion cases. The auxiliary potential is the literal [9,10] distance ramp.

  1. theorem OAI.UniformKServer.HeavyProcess.step_stationary_payment line 17
  2. theorem OAI.UniformKServer.HeavyProcess.step_mover_payment line 28
  3. theorem OAI.UniformKServer.HeavyProcess.run_stationary_payment line 58
  4. theorem OAI.UniformKServer.HeavyProcess.run_mover_payment line 72