BudgetedPrefixLedger.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LowSpaceSubsetSum.BudgetedPrefixController.allowance_le_ledger line 11
Source documentation
The shared-budget allowance is charged to the original full prefix tree, including the exact list of completed checks.
```
theorem allowance_le_ledger (D : RepresentationParentData n) (B : ℕ)
    (collect : StoredRestriction n → StoredEntry.Dictionary D.input D.capacity)
    (hcollect : ∀ P, StoredDictionaryJoin.erase D.input D.capacity (collect P) =
      ({D with maskRestriction := P.semantic}.collect B).state.user)
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.collect, OAI.LowSpaceSubsetSum.StoredRestriction, OAI.LowSpaceSubsetSum.StoredEntry.Dictionary, OAI.LowSpaceSubsetSum.StoredDictionaryJoin.erase