OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationPivotWork.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Counted slice and modular-pivot initialization

Every nonempty row uses two primary-key searches and one modular-pivot search. All three query the same immutable array; no slice is copied. Predicate evaluation costs are separate from the number of queries.

  1. def OAI.LowSpaceSubsetSum.BinarySlice.countedRange line 18
  2. theorem OAI.LowSpaceSubsetSum.BinarySlice.countedRange_value line 32
  3. theorem OAI.LowSpaceSubsetSum.BinarySlice.countedRange_queries line 37
  4. def OAI.LowSpaceSubsetSum.ModularCursor.countedForward line 55
  5. def OAI.LowSpaceSubsetSum.ModularCursor.countedReverse line 60
  6. theorem OAI.LowSpaceSubsetSum.ModularCursor.countedForward_value line 65
  7. theorem OAI.LowSpaceSubsetSum.ModularCursor.countedReverse_value line 69
  8. theorem OAI.LowSpaceSubsetSum.ModularCursor.countedForward_queries line 73
  9. theorem OAI.LowSpaceSubsetSum.ModularCursor.countedReverse_queries line 76
  10. def OAI.LowSpaceSubsetSum.SliceModular.countedForward line 85
  11. def OAI.LowSpaceSubsetSum.SliceModular.countedReverse line 93
  12. theorem OAI.LowSpaceSubsetSum.SliceModular.countedForward_value line 101
  13. theorem OAI.LowSpaceSubsetSum.SliceModular.countedReverse_value line 107
  14. theorem OAI.LowSpaceSubsetSum.SliceModular.countedForward_queries line 113
  15. theorem OAI.LowSpaceSubsetSum.SliceModular.countedReverse_queries line 123
  16. def OAI.LowSpaceSubsetSum.FilteredStream.countedRow line 139
  17. theorem OAI.LowSpaceSubsetSum.FilteredStream.countedRow_value line 151
  18. theorem OAI.LowSpaceSubsetSum.FilteredStream.countedRow_queries line 158
  19. theorem OAI.LowSpaceSubsetSum.FilteredStream.countedRow_index_queries line 183
  20. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.schedule_countedSnapshot_cells line 196