OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionDomains.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Constructing the ten compression domains from a permutation array

The scan reads each domain's original positions, maps them by one array lookup, and sorts the resulting indices into the canonical order expected by raw subset enumeration.

  1. def OAI.LowSpaceSubsetSum.CompressionDomains.positions line 17
  2. def OAI.LowSpaceSubsetSum.CompressionDomains.unsorted line 20
  3. theorem OAI.LowSpaceSubsetSum.CompressionDomains.positions_length line 23
  4. theorem OAI.LowSpaceSubsetSum.CompressionDomains.unsorted_source line 27
  5. theorem OAI.LowSpaceSubsetSum.CompressionDomains.unsorted_nodup line 36
  6. def OAI.LowSpaceSubsetSum.CompressionDomains.domain line 43
  7. theorem OAI.LowSpaceSubsetSum.CompressionDomains.domain_value line 48
  8. theorem OAI.LowSpaceSubsetSum.CompressionDomains.domain_work line 66
  9. def OAI.LowSpaceSubsetSum.CompressionDomains.prepare line 76
  10. theorem OAI.LowSpaceSubsetSum.CompressionDomains.prepare_value line 83
  11. theorem OAI.LowSpaceSubsetSum.CompressionDomains.prepare_work line 90