OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorTraversal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Budgeted depth-first traversal of one separator block

Every node reserves its filter allowance before inspecting record masks. The two recursive branches execute in order, passing the remaining budget; only their Boolean results survive. List lengths are cached in each frame.

  1. def OAI.LowSpaceSubsetSum.BudgetedSeparatorTraversal.execute line 19
  2. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorTraversal.account line 38
  3. def OAI.LowSpaceSubsetSum.BudgetedSeparatorTraversal.reference line 78