CountedPrefixSearch.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Counted depth-first prefix execution

Only the current collector result survives until its overflow test or checker. On overflow the result is discarded before entering either child. The full cost tree is an analysis object; execution skips the second child after YES. Collector and checker implementations carry their own internal costs.

def OAI.LowSpaceSubsetSum.CountedPrefixSearch.run line 18
def OAI.LowSpaceSubsetSum.CountedPrefixSearch.fullCost line 36
Source documentation
The hypothetical full tree includes a sibling skipped after early YES.
```
def fullCost (collect : MaskRestriction n → RecordedDictionary.State (Entry (Fin n)) × ℕ)
    (check : Array (Entry (Fin n)) → Bool × ℕ) (H : ℕ) :
    List (Fin n) → MaskRestriction n → ℕ
  | order, P =>
    let task := collect P
…
```
Mentions: OAI.collect, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.RecordedDictionary.State, OAI.LowSpaceSubsetSum.Entry
theorem OAI.LowSpaceSubsetSum.CountedPrefixSearch.run_value line 48
theorem OAI.LowSpaceSubsetSum.CountedPrefixSearch.run_work line 65
theorem OAI.LowSpaceSubsetSum.CountedPrefixSearch.fullCost_le_ledger line 82
Source documentation
Separate task setup, join counters and completed checker calls. This composes concrete task cost proofs without revisiting the exponential tree.
```
theorem fullCost_le_ledger (D : RepresentationParentData n) (B : ℕ)
    (collect : MaskRestriction n → RecordedDictionary.State (Entry (Fin n)) × ℕ)
    (hcollect : ∀ P, (collect P).1 = ({ D with maskRestriction := P }.collect B).state.user)
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.collect, OAI.LowSpaceSubsetSum.MaskRestriction, OAI.LowSpaceSubsetSum.RecordedDictionary.State, OAI.LowSpaceSubsetSum.Entry