RecordedDictionary.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Bounded dictionaries with an actual array of retained records

structure OAI.LowSpaceSubsetSum.RecordedDictionary.State line 14
def OAI.LowSpaceSubsetSum.RecordedDictionary.empty line 18
def OAI.LowSpaceSubsetSum.RecordedDictionary.feed line 22
Source documentation
The first rejected record is retained, as is its newly allocated trie key. Further callbacks freeze both structures.
```
def feed (C : ℕ) (encode : α → List Bool) (x : α) (r : State α) : State α :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RecordedDictionary.State
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.feed_keys line 27
structure OAI.LowSpaceSubsetSum.RecordedDictionary.Invariant line 30
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.empty_invariant line 35
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.feed_invariant line 39
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.storage line 71
Source documentation
Every stopped state stores at most the capacity plus the rejected record.
```
theorem storage {C width : ℕ} {encode : α → List Bool} {r : State α}
    (hr : Invariant C width encode r) :
    r.records.size ≤ C + 1 ∧ BinaryTrie.nodes r.keys.tree ≤ (width + 1) * (C + 1) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RecordedDictionary.State, OAI.LowSpaceSubsetSum.RecordedDictionary.Invariant, OAI.LowSpaceSubsetSum.BinaryTrie.nodes
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.contains_iff line 78
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.feed_provenance line 83
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.fold_invariant line 95
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.fold_keys line 104
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.fold_fits line 113
Source documentation
A cardinality bound concerns distinct keys, rather than repeated callbacks. When it holds, every supplied record has its key retained in the array.
```
theorem fold_fits {C width : ℕ} (encode : α → List Bool) (xs : List α)
    (U : Finset (List Bool)) (hwidth : ∀ q ∈ U, q.length = width)
    (hcap : U.card ≤ C) (hkeys : ∀ x ∈ xs, encode x ∈ U) :
    let r := xs.foldl (fun r x => feed C encode x r) empty
…
```
Mentions: OAI.LowSpaceSubsetSum.RecordedDictionary.feed, OAI.LowSpaceSubsetSum.RecordedDictionary.empty
def OAI.LowSpaceSubsetSum.RecordedDictionary.callback line 139
Source documentation
The option-valued emitter applies local overlap and prefix checks before an entry is retained. A rejected tuple consumes no dictionary space.
```
def callback {β γ : Type*} (C : ℕ) (encode : α → List Bool)
    (emit : β → γ → Option α) (x : β) (y : γ) (r : State α) : State α × Bool :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RecordedDictionary.State
theorem OAI.LowSpaceSubsetSum.RecordedDictionary.callback_invariant line 143

theorem OAI.LowSpaceSubsetSum.RecordedDictionary.stopped_invariant line 152

Source documentation

Array and trie storage are bounded even at incomplete join prefixes.

theorem stopped_invariant {β γ σ₁ σ₂ : Type*} {C width : ℕ}
    (read₁ : σ₁ → Option (β × σ₁)) (key₁ : β → ℤ)
    (read₂ : σ₂ → Option (γ × σ₂)) (key₂ : γ → ℤ)
    (encode : α → List Bool) (hw : ∀ z, (encode z).length = width)
    (emit : β → γ → Option α) (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂) :
    Invariant C width encode (StreamJoin.stopped read₁ key₁ read₂ key₂
      (callback C encode emit) B fuel₁ fuel₂ controlFuel s₁ s₂ empty).state.user := by
…

Mentions: OAI.LowSpaceSubsetSum.RecordedDictionary.Invariant, OAI.LowSpaceSubsetSum.StreamJoin.stopped, OAI.LowSpaceSubsetSum.RecordedDictionary.callback, OAI.LowSpaceSubsetSum.RecordedDictionary.empty