OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPowerExecution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Constant-state power-of-two initialization

The same executed doubling cursor supplies both prime candidate moduli and trial-division limits.

  1. def OAI.LowSpaceSubsetSum.WordSeedPowerExecution.loop line 13
  2. theorem OAI.LowSpaceSubsetSum.WordSeedPowerExecution.loop_value line 17
  3. def OAI.LowSpaceSubsetSum.WordSeedPowerExecution.run line 28
  4. theorem OAI.LowSpaceSubsetSum.WordSeedPowerExecution.run_value line 30
  5. theorem OAI.LowSpaceSubsetSum.WordSeedPowerExecution.run_work line 33