OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionJoinCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete compression join storage

The common scalar trace is instantiated with the actual tournament readers, weight keys, snapshots and bounded trie callbacks. Shared input arrays are retained by the surrounding pass and are not duplicated here.

  1. def OAI.LowSpaceSubsetSum.CompressionJoinCells.run line 20
  2. theorem OAI.LowSpaceSubsetSum.CompressionJoinCells.value line 33
  3. theorem OAI.LowSpaceSubsetSum.CompressionJoinCells.large line 55
  4. theorem OAI.LowSpaceSubsetSum.CompressionJoinCells.state_bound line 64
  5. theorem OAI.LowSpaceSubsetSum.CompressionJoinCells.snapshot_bound line 74
  6. theorem OAI.LowSpaceSubsetSum.CompressionJoinCells.cells line 91