OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedPreparedSeparator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The budgeted checker for retained dictionary arrays

The preparation expression in the proofs identifies an already-built context. Execution receives its block list and both retained arrays; it does not recompute the context for an individual right dictionary.

  1. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSeparator.reference_value line 19
  2. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSeparator.allowance line 33
  3. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSeparator.value line 59
  4. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSeparator.remaining_bound line 76
  5. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSeparator.accepts line 96