OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredRow.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Modular row initialization with measured weight evaluation

Every binary-search predicate executes the stored-record weight routine. The left weight is computed once, and all searches address the shared right array directly. The resulting cursor is the original filtered row cursor.

  1. def OAI.LowSpaceSubsetSum.BinarySlice.measuredRange line 18
  2. theorem OAI.LowSpaceSubsetSum.BinarySlice.measuredRange_value line 34
  3. theorem OAI.LowSpaceSubsetSum.BinarySlice.measuredRange_work line 40
  4. def OAI.LowSpaceSubsetSum.ModularCursor.measuredForward line 62
  5. def OAI.LowSpaceSubsetSum.ModularCursor.measuredReverse line 68
  6. theorem OAI.LowSpaceSubsetSum.ModularCursor.measuredForward_value line 74
  7. theorem OAI.LowSpaceSubsetSum.ModularCursor.measuredReverse_value line 78
  8. theorem OAI.LowSpaceSubsetSum.ModularCursor.measuredForward_work line 82
  9. theorem OAI.LowSpaceSubsetSum.ModularCursor.measuredReverse_work line 88
  10. def OAI.LowSpaceSubsetSum.SliceModular.measuredForward line 99
  11. def OAI.LowSpaceSubsetSum.SliceModular.measuredReverse line 107
  12. theorem OAI.LowSpaceSubsetSum.SliceModular.measuredForward_value line 115
  13. theorem OAI.LowSpaceSubsetSum.SliceModular.measuredReverse_value line 121
  14. theorem OAI.LowSpaceSubsetSum.SliceModular.measuredForward_work line 127
  15. theorem OAI.LowSpaceSubsetSum.SliceModular.measuredReverse_work line 137
  16. def OAI.LowSpaceSubsetSum.FilteredStream.measuredRow line 153
  17. theorem OAI.LowSpaceSubsetSum.FilteredStream.measuredRow_value line 167
  18. theorem OAI.LowSpaceSubsetSum.FilteredStream.measuredRow_work line 176