OAI/Combinatorics/LowSpaceSubsetSum/Storage/PreparedParentCells.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Prepared contexts throughout the stopped parent collection

Both actual immutable right arrays remain shared during collection. After the join, projection retains only its safe dictionary and scalar counters. The setup routines are accounted for by their own live-cell traces.

  1. def OAI.LowSpaceSubsetSum.PreparedParentCells.runContexts line 17
  2. theorem OAI.LowSpaceSubsetSum.PreparedParentCells.runContexts_value line 26
  3. theorem OAI.LowSpaceSubsetSum.PreparedParentCells.runContexts_cells line 35