MeasuredSortSpace.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Live list and continuation cells of the executed mergesort

The first projection is exactly the measured sort, including its work counter. The second projection records list and continuation storage; comparison callbacks are scalar operations at the terminal application. Input record payloads are shared and are not copied by a list cons.

def OAI.LowSpaceSubsetSum.MeasuredSortSpace.merge line 19
Source documentation
The merge retains its input tails, one continuation per selected head, and the newly constructed result spine.
```
def merge (cmp : α → α → Bool × ℕ) (xs ys : List α) : (List α × ℕ) × ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.MeasuredSortSpace.merge_value line 35
theorem OAI.LowSpaceSubsetSum.MeasuredSortSpace.merge_cells line 45

def OAI.LowSpaceSubsetSum.MeasuredSortSpace.run line 60

Source documentation

One branch runs at a time. The parent input, split spines and completed sibling fit in the eight-cell-per-input local allowance.

def run (cmp : α → α → Bool × ℕ) : ℕ → List α → (List α × ℕ) × ℕ
  | 0, xs => ((xs, 1), xs.length + 2)
  | _ + 1, [] => (([], 1), 2)
  | _ + 1, [x] => (([x], 1), 3)
  | k + 1, x :: y :: rest =>
    let xs := x :: y :: rest
…

theorem OAI.LowSpaceSubsetSum.MeasuredSortSpace.run_value line 73
theorem OAI.LowSpaceSubsetSum.MeasuredSortSpace.run_length line 85
theorem OAI.LowSpaceSubsetSum.MeasuredSortSpace.run_cells line 90