OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorSamplerCells.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Live storage of all bounded separator-family draws

The trace counts accepted packed codes, their list-to-array conversion, and the unused tails of supplied finite seed tuples on failure. The outer application has four rows; no rejection sampler runs without its bound.

  1. def OAI.LowSpaceSubsetSum.SeparatorSamplerCells.family line 18
  2. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.family_value line 31
  3. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.family_cells line 46
  4. def OAI.LowSpaceSubsetSum.SeparatorSamplerCells.materialize line 57
  5. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.materialize_value line 63
  6. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.materialize_cells line 71
  7. def OAI.LowSpaceSubsetSum.SeparatorSamplerCells.rowReserve line 78
  8. def OAI.LowSpaceSubsetSum.SeparatorSamplerCells.run line 80
  9. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.run_value line 94
  10. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.run_cells line 109
  11. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerCells.four_cells line 120