OAI/Combinatorics/LowSpaceSubsetSum/Compression/SampledCompressionTrial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compression from bounded random draws through the stopped residue scan

The sampled permutation is materialized and used by the domain constructor. Every failure branch retains the work already performed. No ideal fallback permutation or prime is evaluated to choose a runtime operation.

  1. def OAI.LowSpaceSubsetSum.SampledCompressionTrial.allowance line 19
  2. def OAI.LowSpaceSubsetSum.SampledCompressionTrial.run line 22
  3. theorem OAI.LowSpaceSubsetSum.SampledCompressionTrial.sound line 32
  4. theorem OAI.LowSpaceSubsetSum.SampledCompressionTrial.work line 50
  5. theorem OAI.LowSpaceSubsetSum.SampledCompressionTrial.accepts line 64
  6. theorem OAI.LowSpaceSubsetSum.SampledCompressionTrial.probability line 74