OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationScalarCells.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Stored-width scalar preparation with explicit sampler memory

These wrappers transport the seed types of the preparation program. Their live-storage annotations preserve the returned values and work counters.

  1. def OAI.LowSpaceSubsetSum.RepresentationScalarCells.nested line 18
  2. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.nested_value line 21
  3. def OAI.LowSpaceSubsetSum.RepresentationScalarCells.draw line 25
  4. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.draw_value line 31
  5. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.draw_cells line 37
  6. def OAI.LowSpaceSubsetSum.RepresentationScalarCells.residues line 42
  7. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.residues_value line 49
  8. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.residues_cells line 57
  9. def OAI.LowSpaceSubsetSum.RepresentationScalarCells.drawResidues line 64
  10. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.drawResidues_value line 70
  11. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.drawResidues_cells line 76
  12. def OAI.LowSpaceSubsetSum.RepresentationScalarCells.extra line 81
  13. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.extra_value line 86
  14. theorem OAI.LowSpaceSubsetSum.RepresentationScalarCells.extra_cells line 91