OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionCallbackCells.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Live storage of the compression dictionary callbacks

The key is constructed once, the trie inserts only a new path, and the cached distinct count controls overflow. The lookup callback retains no new dictionary or list of matches.

  1. def OAI.LowSpaceSubsetSum.CompressionCallbackCells.weightCode line 17
  2. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.weightCode_value line 21
  3. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.weightCode_cells line 26
  4. def OAI.LowSpaceSubsetSum.CompressionCallbackCells.report line 31
  5. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.report_value line 38
  6. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.report_cells line 47
  7. def OAI.LowSpaceSubsetSum.CompressionCallbackCells.probe line 58
  8. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.probe_value line 64
  9. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.probe_cells line 68
  10. def OAI.LowSpaceSubsetSum.CompressionCallbackCells.dictionaryCells line 80
  11. theorem OAI.LowSpaceSubsetSum.CompressionCallbackCells.dictionaryCells_bound line 83