OAI/Combinatorics/LowSpaceSubsetSum/Storage/PrimePreparationCells.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Retaining the stored prefix during bounded nested-prime sampling

Unread candidate vectors are reserved even if prefix preparation rejects. The successful branch calls the exact stored-width scalar sampler.

  1. def OAI.LowSpaceSubsetSum.PrimePreparationCells.run line 18
  2. theorem OAI.LowSpaceSubsetSum.PrimePreparationCells.value line 34
  3. theorem OAI.LowSpaceSubsetSum.PrimePreparationCells.cells_add line 60
  4. theorem OAI.LowSpaceSubsetSum.PrimePreparationCells.cells line 77