BudgetedParentReplay.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Interruptible concrete parent suffix reporting

Each iteration prepays its bounded-mask reader, modular key, validity and dictionary work before any of those implementations is called.

def OAI.LowSpaceSubsetSum.BudgetedParentReplay.run line 16
def OAI.LowSpaceSubsetSum.BudgetedParentReplay.reference line 26
def OAI.LowSpaceSubsetSum.BudgetedParentReplay.execute line 35
theorem OAI.LowSpaceSubsetSum.BudgetedParentReplay.execute_value line 45
theorem OAI.LowSpaceSubsetSum.BudgetedParentReplay.completed_value line 52
theorem OAI.LowSpaceSubsetSum.BudgetedParentReplay.complete line 64
theorem OAI.LowSpaceSubsetSum.BudgetedParentReplay.iteration_charge line 76
theorem OAI.LowSpaceSubsetSum.BudgetedParentReplay.completed_work line 87
theorem OAI.LowSpaceSubsetSum.BudgetedParentReplay.execute_work line 109
Source documentation
The concrete suffix execution respects its prepaid budget even when it times out, with one additional operation for the final failed budget test.
```
theorem execute_work (I : Instance n) (F : IndexedMask n) (P t K : ℤ) (C : ℕ)
    (right : Array (LeafRecord n)) {d : ℕ} (x : CountedParentJoin.Child n)
    (fuel : ℕ) (s : CountedParentJoin.State I F P (.complementary t) right d)
    (a : StoredEntry.Dictionary I C) (budget : ℕ) (hn : 10000 ≤ n) (hd : d ≤ n) :
    (execute I F P t K C right x fuel s a budget).2 ≤ budget + 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.CountedParentJoin.Child, OAI.LowSpaceSubsetSum.CountedParentJoin.State, OAI.LowSpaceSubsetSum.StoredEntry.Dictionary, OAI.LowSpaceSubsetSum.BudgetedParentReplay.execute