OAI/Combinatorics/LowSpaceSubsetSum/Storage/PrefixPreparationCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The complete sampled prefix with retained layout and label arrays

Failed earlier stages reserve the supplied but unread finite seed tails. Successful stages retain the permutation, signs, domains and guesses while materializing the three balanced label arrays. All runtime fields and work counters agree with the canonical preparation.

  1. def OAI.LowSpaceSubsetSum.PrefixPreparationCells.seedReserve line 21
  2. theorem OAI.LowSpaceSubsetSum.PrefixPreparationCells.seedReserve_covers line 23
  3. theorem OAI.LowSpaceSubsetSum.PrefixPreparationCells.reserve_bound line 36
  4. def OAI.LowSpaceSubsetSum.PrefixPreparationCells.assemble line 58
  5. def OAI.LowSpaceSubsetSum.PrefixPreparationCells.run line 74
  6. theorem OAI.LowSpaceSubsetSum.PrefixPreparationCells.value line 82
  7. theorem OAI.LowSpaceSubsetSum.PrefixPreparationCells.sum_bound line 101
  8. theorem OAI.LowSpaceSubsetSum.PrefixPreparationCells.assemble_cells line 117
  9. theorem OAI.LowSpaceSubsetSum.PrefixPreparationCells.cells line 134