OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedMaskExecution.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Building sampled subsets from stored permutation entries

The sampled permutation is materialized and its first selected entries are scanned into a duplicate-free list. The Finset constructor uses that list without a further deduplication pass.

  1. abbrev OAI.LowSpaceSubsetSum.WordSeedMeasured.PermutationAccepted line 18
  2. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.permutation_materializes line 20
  3. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.permutation_materialized_value line 31
  4. abbrev OAI.LowSpaceSubsetSum.WordSeedMeasured.Materialized line 41
  5. def OAI.LowSpaceSubsetSum.WordSeedMeasured.materializeAccepted line 45
  6. def OAI.LowSpaceSubsetSum.WordSeedMeasured.selectedCompute line 54
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.selectedCompute_value line 70
  8. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.selectedCompute_work line 82
  9. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.selectedCompute_cells line 94
  10. def OAI.LowSpaceSubsetSum.WordSeedMeasured.selectedTyped line 107
  11. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.selectedTyped_value line 114
  12. def OAI.LowSpaceSubsetSum.WordSeedMeasured.subsetInitial line 119
  13. def OAI.LowSpaceSubsetSum.WordSeedMeasured.fixedSize line 124
  14. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.fixedSize_bounded line 129