OAI/Combinatorics/LowSpaceSubsetSum/Storage/MeasuredReaderCells.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Live cells of tournament path replacement

The input tree and its untouched siblings remain shared. Each recursive frame retains one path position; the trace includes both the old tree and the new path while keys are evaluated. It never materializes candidate lists.

  1. def OAI.LowSpaceSubsetSum.MeasuredReaderCells.pick line 16
  2. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.pick_value line 24
  3. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.pick_cells line 28
  4. def OAI.LowSpaceSubsetSum.MeasuredReaderCells.replace line 41
  5. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.replace_value line 57
  6. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.replace_step_bound line 66
  7. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.replace_cells line 78
  8. def OAI.LowSpaceSubsetSum.MeasuredReaderCells.advance line 94
  9. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.advance_value line 108
  10. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.advance_cells line 118
  11. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.advance_refines line 147
  12. def OAI.LowSpaceSubsetSum.MeasuredReaderCells.next line 157
  13. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.next_value line 176
  14. theorem OAI.LowSpaceSubsetSum.MeasuredReaderCells.next_cells line 213