DictionaryCallback.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

A bounded dictionary callback for the actual stream join

The callback freezes after the first capacity violation. It always lets the join continue, so the established complete-join theorem applies on every outcome. The overflowing residue is discarded afterwards. Completing the scan uses only the bounded Cartesian potential and no extra keys.

def OAI.LowSpaceSubsetSum.BinaryTrie.feed line 17
def OAI.LowSpaceSubsetSum.BinaryTrie.callback line 24
theorem OAI.LowSpaceSubsetSum.BinaryTrie.feed_frozen line 28
structure OAI.LowSpaceSubsetSum.BinaryTrie.Safe line 31
theorem OAI.LowSpaceSubsetSum.BinaryTrie.empty_safe line 37
theorem OAI.LowSpaceSubsetSum.BinaryTrie.feed_safe line 40
theorem OAI.LowSpaceSubsetSum.BinaryTrie.feed_nodes line 62

theorem OAI.LowSpaceSubsetSum.BinaryTrie.feed_fits line 71

Source documentation

The cardinality hypothesis is on the actual possible key set, not the number of callbacks. Duplicate occurrences never consume extra capacity.

theorem feed_fits {C width : ℕ} {r : BuildResult} {U : Finset (List Bool)}
    (hclear : r.overflow = false) (ht : HasWidth r.tree width)
    (hwidth : ∀ key ∈ U, key.length = width) (htU : keySet r.tree ⊆ U)
    (hcap : U.card ≤ C) {key : List Bool} (hkey : key ∈ U) :
    (feed C key r).overflow = false ∧
      keySet (feed C key r).tree = Insert.insert key (keySet r.tree) ∧
      (feed C key r).processed = r.processed + 1 ∧
      HasWidth (feed C key r).tree width := by
…

Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.BuildResult, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.keySet, OAI.LowSpaceSubsetSum.BinaryTrie.feed

theorem OAI.LowSpaceSubsetSum.BinaryTrie.fold_fits line 95
theorem OAI.LowSpaceSubsetSum.BinaryTrie.fold_safe line 121

def OAI.LowSpaceSubsetSum.BinaryTrie.matchingKeys line 130

Source documentation

Proof-only list of keys reported by a complete Cartesian-match join.

def matchingKeys {α β : Type*} (key₁ : α → ℤ) (key₂ : β → ℤ)
    (encode : α → β → List Bool) (xs : List α) (ys : List β) : List (List Bool) :=
…

theorem OAI.LowSpaceSubsetSum.BinaryTrie.mem_matchingKeys line 134
theorem OAI.LowSpaceSubsetSum.BinaryTrie.matchFold_eq_keys line 140
theorem OAI.LowSpaceSubsetSum.BinaryTrie.matchFold_fits line 150
theorem OAI.LowSpaceSubsetSum.BinaryTrie.matchFold_safe line 168

theorem OAI.LowSpaceSubsetSum.BinaryTrie.join_fits line 180

Source documentation

Exact membership after the actual finite-state stream join. The only capacity assumption is the cardinality of a universe containing its keys.

theorem join_fits {α β σ₁ σ₂ : Type*} {C width : ℕ}
    (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
    (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (encode : α → β → List Bool)
    (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
    (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
    (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂)
    (hsort₁ : (view₁ s₁).Pairwise (fun x y => key₁ x ≤ key₁ y))
    (hsort₂ : (view₂ s₂).Pairwise (fun x y => key₂ x ≤ key₂ y))
    (hcap₁ : (view₁ s₁).length ≤ fuel₁) (hcap₂ : (view₂ s₂).length ≤ fuel₂)
    (hfuel : (view₁ s₁).length + (view₂ s₂).length < controlFuel)
    (U : Finset (List Bool)) (hwidth : ∀ key ∈ U, key.length = width) (hcap : U.card ≤ C)
    (hkeys : ∀ x ∈ view₁ s₁, ∀ y ∈ view₂ s₂, key₁ x = key₂ y → encode x y ∈ U) :
…

Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader

theorem OAI.LowSpaceSubsetSum.BinaryTrie.join_nodes line 210

Source documentation

Every complete join, including an overflowing residue, retains at most one rejected key beyond capacity. This gives the concrete trie node bound.

theorem join_nodes {α β σ₁ σ₂ : Type*} {C width : ℕ}
    (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
    (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ) (encode : α → β → List Bool)
    (view₁ : σ₁ → List α) (hread₁ : RowMerge.IsReader read₁ view₁)
    (view₂ : σ₂ → List β) (hread₂ : RowMerge.IsReader read₂ view₂)
    (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂)
    (hsort₁ : (view₁ s₁).Pairwise (fun x y => key₁ x ≤ key₁ y))
    (hsort₂ : (view₂ s₂).Pairwise (fun x y => key₂ x ≤ key₂ y))
    (hcap₁ : (view₁ s₁).length ≤ fuel₁) (hcap₂ : (view₂ s₂).length ≤ fuel₂)
    (hfuel : (view₁ s₁).length + (view₂ s₂).length < controlFuel)
    (hwidth : ∀ x ∈ view₁ s₁, ∀ y ∈ view₂ s₂,
      key₁ x = key₂ y → (encode x y).length = width) :
…

Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader