OAI/Combinatorics/LowSpaceSubsetSum/Streams/DictionaryProvenance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Provenance of every retained bounded-dictionary key

Capacity failure can freeze a callback, but cannot create an unreported key. The proof applies even to overflowing complete joins, with no cardinality hypothesis on a bucket and no knowledge of any solution.

  1. theorem OAI.LowSpaceSubsetSum.BinaryTrie.feed_provenance line 15
  2. theorem OAI.LowSpaceSubsetSum.BinaryTrie.fold_provenance line 30
  3. theorem OAI.LowSpaceSubsetSum.BinaryTrie.matchFold_provenance line 45
  4. theorem OAI.LowSpaceSubsetSum.BinaryTrie.join_provenance line 63