OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedCompressionExecution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual word-driven compression sampler

The permutation generator retains its range candidate buffers. The prime width is computed by one multiplication and one division before its modulus and bounded rejection routine. Exhaustion remains none.

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.compressionCore line 16
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.compression line 25
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.compressionWork line 33
  4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.compression_bounded line 38