OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPermutationExecution.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measured permutation seed generation

Each range call computes its modulus, draws and retains the actual candidate tuple, and caches its accepted digit. Permutation values are composition closures; their application or array materialization remains a separate measured operation, as in PermutationArray.

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.permutation line 16
  2. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.permutation_bounded line 34