OAI/Combinatorics/LowSpaceSubsetSum/Counting/SliceModular.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Modular pivot readers on shared-array slices

Binary pivot queries and subsequent cyclic reads access the same immutable array through the slice address map. No reordered slice is stored. Empty, direct and complementary rows all use the same constant-size cursor type.

  1. def OAI.LowSpaceSubsetSum.SliceModular.forward line 19
  2. def OAI.LowSpaceSubsetSum.SliceModular.reverse line 26
  3. theorem OAI.LowSpaceSubsetSum.SliceModular.forward_output line 33
  4. theorem OAI.LowSpaceSubsetSum.SliceModular.reverse_output line 46
  5. theorem OAI.LowSpaceSubsetSum.SliceModular.forward_perm line 59
  6. theorem OAI.LowSpaceSubsetSum.SliceModular.reverse_perm line 66
  7. theorem OAI.LowSpaceSubsetSum.SliceModular.forward_sorted line 73
  8. theorem OAI.LowSpaceSubsetSum.SliceModular.reverse_sorted line 84