OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredMaskCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Bounded masks constructed by the measured subset generators

The returned masks retain the generated index lists. The wrapping phase counts the old family, the new list spine, and all bounded mask payloads. Neither phase constructs finite sets.

  1. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.select_length line 17
  2. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.all_length line 22
  3. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.wrap_eq line 27
  4. def OAI.LowSpaceSubsetSum.StoredMaskCells.select line 34
  5. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.select_value line 42
  6. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.select_cells line 52
  7. def OAI.LowSpaceSubsetSum.StoredMaskCells.all line 69
  8. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.all_value line 77
  9. theorem OAI.LowSpaceSubsetSum.StoredMaskCells.all_cells line 87