OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionDomainCells.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Live cells for the ten concrete compression domains

Only arithmetic interval tests, stored permutation lookups and list sorts are executed. Completed domains are retained while subsequent rows are constructed, and the source finite sets appear only in the value theorem.

  1. def OAI.LowSpaceSubsetSum.CompressionDomainCells.run line 17
  2. theorem OAI.LowSpaceSubsetSum.CompressionDomainCells.value line 27
  3. theorem OAI.LowSpaceSubsetSum.CompressionDomainCells.cells line 32