OAI/Combinatorics/LowSpaceSubsetSum/Streams/CountedSort.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A counted implementation of the sort used by the streams

The merge follows each comparison branch and counts its steps. The bounded recursive sort is exactly List.mergeSort once its depth accommodates the input length. Its ledger includes list-length/split scans and merge work, giving a linear cost per recursion level, without a quadratic sorting bound.

  1. def OAI.LowSpaceSubsetSum.CountedSort.merge line 21
  2. theorem OAI.LowSpaceSubsetSum.CountedSort.merge_value line 34
  3. theorem OAI.LowSpaceSubsetSum.CountedSort.merge_steps line 44
  4. def OAI.LowSpaceSubsetSum.CountedSort.run line 62
  5. theorem OAI.LowSpaceSubsetSum.CountedSort.run_length line 74
  6. theorem OAI.LowSpaceSubsetSum.CountedSort.run_value line 89
  7. theorem OAI.LowSpaceSubsetSum.CountedSort.run_steps line 123
  8. def OAI.LowSpaceSubsetSum.CountedSort.sort line 149
  9. theorem OAI.LowSpaceSubsetSum.CountedSort.sort_value line 152
  10. theorem OAI.LowSpaceSubsetSum.CountedSort.sort_steps line 156
  11. theorem OAI.LowSpaceSubsetSum.CountedSort.sort_steps_of_index_bits line 160