BudgetedOuterReplay.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Outer replay with a budgeted inner callback

The fixed charge covers one outer read/key step. A callback receives the remaining allowance and returns its unspent part. This is the control used when one outer occurrence triggers a buffered Cartesian replay.

def OAI.LowSpaceSubsetSum.BudgetedOuterReplay.execute line 17
theorem OAI.LowSpaceSubsetSum.BudgetedOuterReplay.execute_value line 45

theorem OAI.LowSpaceSubsetSum.BudgetedOuterReplay.execute_work line 95

Source documentation

Both successful and interrupted inner replays are covered.

theorem execute_work (read : σ → Option (α × σ) × ℕ) (key : α → ℤ × ℕ) (K : ℤ)
    (report : α → τ → ℕ → Option ((τ × Bool) × ℕ) × ℕ) (R L charge : ℕ)
    (hr : ∀ s, (read s).2 ≤ R) (hk : ∀ x, (key x).2 ≤ L)
    (hcharge : R + L + 8 ≤ charge)
    (hwork : ∀ x a b, (report x a b).2 ≤ b + 1)
    (hspent : ∀ x a b v left, (report x a b).1 = some (v, left) →
      left ≤ b ∧ (report x a b).2 ≤ b - left)
    (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ) :
    (execute charge read key K report fuel s a q r budget).2 ≤ budget + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.BudgetedOuterReplay.execute

theorem OAI.LowSpaceSubsetSum.BudgetedOuterReplay.execute_spent line 133