OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationFromFamilies.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Passing the executed family arrays into the stopped representation trial

The prefix history supplies layout, partitions, moduli and residues. The last random stage constructs actual arrays, which are retained directly by the incidence-table builder and the subsequent stopped residue schedule.

  1. abbrev OAI.LowSpaceSubsetSum.RepresentationFromFamilies.width line 19
  2. def OAI.LowSpaceSubsetSum.RepresentationFromFamilies.schedule line 21
  3. def OAI.LowSpaceSubsetSum.RepresentationFromFamilies.parameters line 26
  4. def OAI.LowSpaceSubsetSum.RepresentationFromFamilies.run line 30
  5. theorem OAI.LowSpaceSubsetSum.RepresentationFromFamilies.value line 46
  6. theorem OAI.LowSpaceSubsetSum.RepresentationFromFamilies.work line 74
  7. theorem OAI.LowSpaceSubsetSum.RepresentationFromFamilies.accepts line 102
  8. theorem OAI.LowSpaceSubsetSum.RepresentationFromFamilies.sound line 147