OAI/Combinatorics/LowSpaceSubsetSum/Counting/ParentLiveState.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Payload bounds for every live stored parent state

These bounds use the intrinsic bounded-mask and safe-dictionary types. They apply to intermediate callback states and reader snapshots, including after the first overflowing insertion.

  1. def OAI.LowSpaceSubsetSum.ParentLiveState.reader line 16
  2. theorem OAI.LowSpaceSubsetSum.ParentLiveState.reader_exact line 20
  3. def OAI.LowSpaceSubsetSum.ParentLiveState.dictionary line 25
  4. theorem OAI.LowSpaceSubsetSum.ParentLiveState.list_cells line 29
  5. theorem OAI.LowSpaceSubsetSum.ParentLiveState.dictionary_le line 38
  6. theorem OAI.LowSpaceSubsetSum.ParentLiveState.dictionary_scale line 48
  7. def OAI.LowSpaceSubsetSum.ParentLiveState.sharedArrays line 55
  8. theorem OAI.LowSpaceSubsetSum.ParentLiveState.sharedArrays_le line 58
  9. def OAI.LowSpaceSubsetSum.ParentLiveState.frame line 63
  10. theorem OAI.LowSpaceSubsetSum.ParentLiveState.frame_le line 70