MeasuredSeparatorTraversal.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Executed separator DFS with measured interval callbacks

Both child calls follow the source traversal exactly. Filtering is a concrete tail-recursive loop over retained record pointers. Its callback charge includes the stored-mask lookup and the two binary searches.

def OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.keep line 17
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.keep_value line 20
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.keep_work line 27
def OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.run line 33
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.run_value line 55
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.empty_bound line 82
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.leaf_bound line 89
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.branch_bound line 95
theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.nonempty_size line 103

theorem OAI.LowSpaceSubsetSum.MeasuredSeparatorTraversal.run_work line 123

Source documentation

The existing source scans absorb every measured filter and branch action.

theorem run_work (test₁ : α → ℕ → ℕ → Bool × ℕ)
    (test₂ : β → ℕ → ℕ → Bool × ℕ)
    (inc₁ : α → Array ℕ) (inc₂ : β → Array ℕ)
    (ht₁ : ∀ x lo hi, (test₁ x lo hi).1 = SeparatorIncidenceTable.hit (inc₁ x) lo hi)
    (ht₂ : ∀ y lo hi, (test₂ y lo hi).1 = SeparatorIncidenceTable.hit (inc₂ y) lo hi)
    (K L : ℕ) (hc₁ : ∀ x lo hi, (test₁ x lo hi).2 ≤ K)
    (hc₂ : ∀ y lo hi, (test₂ y lo hi).2 ≤ K)
    (leaf : ℕ → List α → List β → Bool × ℕ)
    (source : ℕ → List α → List β → SeparatorTraversal.Result)
    (hleaf : ∀ j xs ys, (leaf j xs ys).2 ≤
      L * ((source j xs ys).scans + xs.length + ys.length + 1))
    (k lo hi : ℕ) (xs : List α) (ys : List β) :
…

Mentions: OAI.LowSpaceSubsetSum.SeparatorIncidenceTable.hit, OAI.LowSpaceSubsetSum.SeparatorTraversal.Result