OAI/Combinatorics/UniformKServer/StarEnergy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The sole law-dependent energy is the actual hidden child-count movement. Posterior drift is derived by conditional contraction, never assumed.

  1. def OAI.UniformKServer.StarEnergy.integral line 18
  2. theorem OAI.UniformKServer.StarEnergy.integral_mono line 21
  3. theorem OAI.UniformKServer.StarEnergy.integral_nonneg line 25
  4. theorem OAI.UniformKServer.StarEnergy.integral_add line 29
  5. theorem OAI.UniformKServer.StarEnergy.integral_mul line 33
  6. theorem OAI.UniformKServer.StarEnergy.integral_sum line 37
  7. def OAI.UniformKServer.StarEnergy.countMove line 42
  8. def OAI.UniformKServer.StarEnergy.cost line 43
  9. def OAI.UniformKServer.StarEnergy.allowance line 44
  10. def OAI.UniformKServer.StarEnergy.energy line 45
  11. theorem OAI.UniformKServer.StarEnergy.cost_nonneg line 47
  12. theorem OAI.UniformKServer.StarEnergy.allowance_bounds line 50
  13. theorem OAI.UniformKServer.StarEnergy.energy_nonneg line 62
  14. theorem OAI.UniformKServer.StarEnergy.cost_le_energy line 65
  15. theorem OAI.UniformKServer.StarEnergy.allowance_le_energy line 68
  16. theorem OAI.UniformKServer.StarEnergy.rank_drift line 71
  17. theorem OAI.UniformKServer.StarEnergy.child_drift line 83
  18. theorem OAI.UniformKServer.StarEnergy.parent_drift line 90
  19. theorem OAI.UniformKServer.StarEnergy.hidden_move line 100