OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedFactorExecution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Initialized nested-prime seed execution

Widths below four use the constant unit factor. Every larger factor executes its modulus construction, actual bounded prime test, and retained candidate buffer. Tuple assembly has an explicit fixed charge.

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.factorWork line 18
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.factor line 21
  3. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.factor_bounded line 34
  4. def OAI.LowSpaceSubsetSum.WordSeedMeasured.triplePrime line 58
  5. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.triplePrime_bounded line 68