OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPrimeTestExecution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Prime testing with executed scalar initialization

Both powers used by the test are produced by the doubling cursor. The divisor scan consumes the computed limit directly and retains scalar state.

  1. def OAI.LowSpaceSubsetSum.WordSeedPrimeTestExecution.run line 14
  2. theorem OAI.LowSpaceSubsetSum.WordSeedPrimeTestExecution.run_value line 21
  3. theorem OAI.LowSpaceSubsetSum.WordSeedPrimeTestExecution.run_work line 27
  4. theorem OAI.LowSpaceSubsetSum.WordSeedPrimeTestExecution.run_cells line 35