OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedModulusExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Computing a rejection range width and its cached modulus

A doubling cursor starts at one and stops at the first power of two at least the requested range size. The width and modulus are computed together.

  1. structure OAI.LowSpaceSubsetSum.WordSeedModulusExecution.Result line 13
  2. def OAI.LowSpaceSubsetSum.WordSeedModulusExecution.loop line 18
  3. theorem OAI.LowSpaceSubsetSum.WordSeedModulusExecution.loop_value line 24
  4. def OAI.LowSpaceSubsetSum.WordSeedModulusExecution.run line 55
  5. theorem OAI.LowSpaceSubsetSum.WordSeedModulusExecution.run_value line 57
  6. theorem OAI.LowSpaceSubsetSum.WordSeedModulusExecution.run_width line 62
  7. theorem OAI.LowSpaceSubsetSum.WordSeedModulusExecution.run_modulus line 64
  8. theorem OAI.LowSpaceSubsetSum.WordSeedModulusExecution.run_work line 66
  9. theorem OAI.LowSpaceSubsetSum.WordSeedModulusExecution.run_modulus_fits line 68