OAI/Combinatorics/UniformKServer/SideRecurrence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Persistent causal selection of the two actual side minimizers. Empty side domains and D=0 use the same compact update, with the source's free deletion.

  1. def OAI.UniformKServer.SideRecurrence.StepSpec line 17
  2. def OAI.UniformKServer.SideRecurrence.chooseStep line 25
  3. theorem OAI.UniformKServer.SideRecurrence.zero_state line 29
  4. theorem OAI.UniformKServer.SideRecurrence.chooseStep_spec line 32
  5. def OAI.UniformKServer.SideRecurrence.trajectory line 48
  6. def OAI.UniformKServer.SideRecurrence.prepared line 53
  7. def OAI.UniformKServer.SideRecurrence.InputValid line 57
  8. theorem OAI.UniformKServer.SideRecurrence.trajectory_state line 64
  9. theorem OAI.UniformKServer.SideRecurrence.trajectory_step line 74
  10. theorem OAI.UniformKServer.SideRecurrence.causal_through line 83