OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationBucketProgram.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

One actual residue bucket: left retention and right prefix search

  1. structure OAI.LowSpaceSubsetSum.RepresentationBucketData line 9
  2. def OAI.LowSpaceSubsetSum.RepresentationBucketData.target line 19
  3. def OAI.LowSpaceSubsetSum.RepresentationBucketData.check line 22
  4. def OAI.LowSpaceSubsetSum.RepresentationBucketData.run line 28

    Source documentation

    The left array is retained while each right task regenerates its own restricted leaves and streams. An empty or overflowing left task is skipped.

    def run (B : ℕ) (families : Fin 4 → Array (Finset (Fin g))) : Bool :=
…
  5. theorem OAI.LowSpaceSubsetSum.RepresentationBucketData.sound line 34