DictionaryPrefixes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Dictionary space at every stopped join prefix

The callback invariant is preserved inside buffer replay, suffix replay, tie-group replay, and the outer join loop. Thus the storage bound holds at every watchdog cutoff, without assuming that a join completes.

theorem OAI.LowSpaceSubsetSum.DictionaryPrefixes.one_preserves line 15
theorem OAI.LowSpaceSubsetSum.DictionaryPrefixes.group_preserves line 32
theorem OAI.LowSpaceSubsetSum.DictionaryPrefixes.step_preserves line 50
theorem OAI.LowSpaceSubsetSum.DictionaryPrefixes.run_preserves line 77

theorem OAI.LowSpaceSubsetSum.DictionaryPrefixes.stopped_safe line 91

Source documentation

No reader law, sortedness, completeness, or probability event is needed for the dictionary-space invariant at a stopped control prefix.

theorem stopped_safe {α β σ₁ σ₂ : Type*} {C width : ℕ}
    (read₁ : σ₁ → Option (α × σ₁)) (key₁ : α → ℤ)
    (read₂ : σ₂ → Option (β × σ₂)) (key₂ : β → ℤ)
    (encode : α → β → List Bool) (hwidth : ∀ x y, (encode x y).length = width)
    (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂) :
    BinaryTrie.Safe C width (StreamJoin.run read₁ key₁ read₂ key₂
      (BinaryTrie.callback C encode) B fuel₁ fuel₂ controlFuel s₁ s₂ ⟨.empty, false, 0⟩).user := by
…

Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Safe, OAI.LowSpaceSubsetSum.StreamJoin.run, OAI.LowSpaceSubsetSum.BinaryTrie.callback

theorem OAI.LowSpaceSubsetSum.DictionaryPrefixes.stopped_nodes line 103