OAI/Combinatorics/LowSpaceSubsetSum/Storage/LayoutPreparationCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Executed canonical layout preparation and its retained arrays

The sampled permutation and sign mask remain live while the three mixer counts and integer widths are prepared. The mixer preparation already accounts for its shared arrays and merge state.

  1. def OAI.LowSpaceSubsetSum.LayoutPreparationCells.assemble line 19
  2. def OAI.LowSpaceSubsetSum.LayoutPreparationCells.run line 31
  3. theorem OAI.LowSpaceSubsetSum.LayoutPreparationCells.value line 37
  4. theorem OAI.LowSpaceSubsetSum.LayoutPreparationCells.scalar_bound line 46
  5. theorem OAI.LowSpaceSubsetSum.LayoutPreparationCells.assemble_cells line 64
  6. theorem OAI.LowSpaceSubsetSum.LayoutPreparationCells.raw_bound line 81
  7. theorem OAI.LowSpaceSubsetSum.LayoutPreparationCells.cells line 98