OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedStoppedJoin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A watchdog for the complete stopped join

Each iteration reserves its own fixed control cost before invoking the prepaid stream step. The reference allowance is used only in proofs; execution inspects only its fuel, state, and remaining budget.

  1. def OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.execute line 20
  2. def OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.reference line 37
  3. def OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.allowance line 44
  4. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.execute_value line 49
  5. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.execute_work line 85
  6. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.execute_spent line 111
  7. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.execute_complete line 149
  8. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.allowance_potential line 174

    Source documentation

    Telescoping the bills pays only for operations that the reference performs.

    theorem allowance_potential (pure : State → State) (bill : State → ℕ)
    (potential : State → ℕ) (extra : ℕ)
    (hb : ∀ st, bill st + potential st ≤ potential (pure st) + extra)
    (fuel : ℕ) (st : State) :
    allowance pure bill fuel st + potential st ≤
      potential (reference pure fuel st).state + (extra + 4) * (reference pure fuel st).steps + 4 := by
…

    Mentions: OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.allowance, OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.reference

  9. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedJoin.execute_remaining line 190