OAI/Combinatorics/LowSpaceSubsetSum/Storage/BackgroundBlockCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Copying the eight background rows from their shared array

Each read uses the computed prefix-sum offset. Rows are retained once in an explicit vector, and the returned view indexes that vector.

  1. def OAI.LowSpaceSubsetSum.BackgroundBlockCells.index line 16
  2. theorem OAI.LowSpaceSubsetSum.BackgroundBlockCells.index_value line 22
  3. def OAI.LowSpaceSubsetSum.BackgroundBlockCells.row line 28
  4. theorem OAI.LowSpaceSubsetSum.BackgroundBlockCells.row_value line 34
  5. def OAI.LowSpaceSubsetSum.BackgroundBlockCells.run line 39
  6. theorem OAI.LowSpaceSubsetSum.BackgroundBlockCells.value line 46
  7. theorem OAI.LowSpaceSubsetSum.BackgroundBlockCells.row_work line 55
  8. theorem OAI.LowSpaceSubsetSum.BackgroundBlockCells.cells line 62