BoundedDictionary.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Streaming construction of a hard-capacity dictionary

The input is a list of occurrences; equal keys are tested and skipped. The builder stops at the first new key beyond capacity. Its tree includes the possibly allocated rejected key, as in the manuscript's implementation. No Cartesian product or ambient entry set is stored by this procedure.

structure OAI.LowSpaceSubsetSum.BinaryTrie.BuildResult line 16
def OAI.LowSpaceSubsetSum.BinaryTrie.tick line 21
def OAI.LowSpaceSubsetSum.BinaryTrie.build line 23
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_processed_le line 32
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_hasWidth line 44
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_compact line 61
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_entries_le line 75
Source documentation
The capacity is respected on every outcome, including overflow and early termination. At most one extra key has been allocated.
```
theorem build_entries_le {C width : ℕ} {t : Tree} {keys : List (List Bool)}
    (ht : HasWidth t width) (hk : ∀ key ∈ keys, key.length = width)
    (hcap : entries t ≤ C) : entries (build C t keys).tree ≤ C + 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.entries, OAI.LowSpaceSubsetSum.BinaryTrie.build
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_overflow_entries line 98
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_complete_contains_iff line 124
Source documentation
A completed build retains exactly the original keys and the input keys, regardless of how many duplicate occurrences were streamed.
```
theorem build_complete_contains_iff {C width : ℕ} {t : Tree}
    {keys : List (List Bool)} (ht : HasWidth t width)
    (hk : ∀ key ∈ keys, key.length = width)
    (hcomplete : (build C t keys).overflow = false)
    {query : List Bool} (hq : query.length = width) :
    contains (build C t keys).tree query = true ↔
      contains t query = true ∨ query ∈ keys := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.build, OAI.LowSpaceSubsetSum.BinaryTrie.contains
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_nodes_le line 155
Source documentation
Concrete live-trie space, with the first rejected key included.
```
theorem build_nodes_le {C width : ℕ} {t : Tree} {keys : List (List Bool)}
    (ht : HasWidth t width) (hc : Compact t)
    (hk : ∀ key ∈ keys, key.length = width) (hcap : entries t ≤ C) :
    nodes (build C t keys).tree ≤ (width + 1) * (C + 1) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.Compact, OAI.LowSpaceSubsetSum.BinaryTrie.entries, OAI.LowSpaceSubsetSum.BinaryTrie.nodes, OAI.LowSpaceSubsetSum.BinaryTrie.build