OAI/Combinatorics/LowSpaceSubsetSum/Storage/MeasuredBuildCells.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Live cells during direct tournament initialization

The left subtree remains live while the right subtree is constructed. A parent shares the completed children; it does not copy their payloads.

  1. def OAI.LowSpaceSubsetSum.MeasuredBuildCells.run line 16
  2. theorem OAI.LowSpaceSubsetSum.MeasuredBuildCells.run_value line 30
  3. theorem OAI.LowSpaceSubsetSum.MeasuredBuildCells.step_bound line 38
  4. theorem OAI.LowSpaceSubsetSum.MeasuredBuildCells.run_cells line 57