OAI/Combinatorics/UniformKServer/StarMovementBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complete actual local movement theorem. Parent movement has coefficient one; the absolute large coefficient multiplies only the hidden count movement. The additive allowance is independent of both the law and the horizon.

  1. theorem OAI.UniformKServer.StarMovementBudget.initial_budget line 20
  2. theorem OAI.UniformKServer.StarMovementBudget.expense_budget line 26
  3. theorem OAI.UniformKServer.StarMovementBudget.movement line 46