OAI/Combinatorics/LowSpaceSubsetSum/Word/WordWidthBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed word widths, watchdog counters and memory addresses

These are arithmetic bounds on the manuscript's concrete finite cutoffs. They do not assert that the algorithm has been compiled to a RAM program.

  1. def OAI.LowSpaceSubsetSum.wordWidth line 16
  2. def OAI.LowSpaceSubsetSum.trialWatchdog line 18
  3. def OAI.LowSpaceSubsetSum.writableWordLimit line 21
  4. theorem OAI.LowSpaceSubsetSum.guarded_polynomial_exponential line 24
  5. theorem OAI.LowSpaceSubsetSum.trialWatchdog_lt_two_pow line 39
  6. theorem OAI.LowSpaceSubsetSum.writableWordLimit_lt_two_pow line 58
  7. theorem OAI.LowSpaceSubsetSum.cutoff_fits_word line 77