OAI/Combinatorics/LowSpaceSubsetSum/Counting/ParentLiveBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform payload bounds for all concrete parent states

The estimates use the stored type invariants, so an interrupted join and an already overflowing dictionary satisfy the same bounds as a completed run. Shared input arrays are counted once outside the mutable state.

  1. theorem OAI.LowSpaceSubsetSum.ParentLiveBounds.reader_le line 16
  2. theorem OAI.LowSpaceSubsetSum.ParentLiveBounds.frame_le line 26
  3. theorem OAI.LowSpaceSubsetSum.ParentLiveBounds.shared_le line 40
  4. theorem OAI.LowSpaceSubsetSum.ParentLiveBounds.all_inputs_and_state line 49