RepresentationStreamWork.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Occurrence counts and stopped query ledgers for concrete parent streams

The list and finite-set views below are proof objects. Runtime still uses the shared leaf arrays and constant-state tournament readers.

theorem OAI.LowSpaceSubsetSum.FilteredStream.product_filter_bag line 19
theorem OAI.LowSpaceSubsetSum.FilteredStream.sorted_output_perm line 31
Source documentation
The actual output is a permutation of the filtered indexed Cartesian product, so equal numerical weights do not collapse occurrence identities.
```
theorem sorted_output_perm (left : Array α) (right : Array β)
    (wl : α → ℤ) (wr : β → ℤ) (p P c : ℤ) (hP : 0 < P) (mode : Mode) :
    (MergedReader.output (key wl wr P mode) (read (ResidueSort.sort right wr p P))
      (view (ResidueSort.sort right wr p P)) (sortedStart left right wl wr p P c hP mode)).Perm
      ((left.toList ×ˢ right.toList).filter
        (fun z => decide ((wl z.1 + wr z.2) % p = c % p))) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.FilteredStream.Mode, OAI.LowSpaceSubsetSum.MergedReader.output, OAI.LowSpaceSubsetSum.FilteredStream.key, OAI.LowSpaceSubsetSum.FilteredStream.read, OAI.LowSpaceSubsetSum.ResidueSort.sort, OAI.LowSpaceSubsetSum.FilteredStream.view, OAI.LowSpaceSubsetSum.FilteredStream.sortedStart
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_perm line 51
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_nodup line 58
def OAI.LowSpaceSubsetSum.RepresentationPairData.outputUniverse line 63
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_toFinset line 69
theorem OAI.LowSpaceSubsetSum.RepresentationPairData.output_length_eq_card line 75

theorem OAI.LowSpaceSubsetSum.MatchPotential.count_eq_filter_product_length line 85

Source documentation

Cartesian occurrence identity for the actual join potential.

theorem count_eq_filter_product_length (key₁ : α → ℤ) (key₂ : β → ℤ)
    (xs : List α) (ys : List β) :
    count key₁ key₂ xs ys =
      ((xs ×ˢ ys).filter (fun z => decide (key₁ z.1 = key₂ z.2))).length := by
…

Mentions: OAI.LowSpaceSubsetSum.MatchPotential.count

def OAI.LowSpaceSubsetSum.RepresentationParentData.matchingUniverse line 102
Source documentation
Raw matching occurrences include those rejected by the validity callback.
```
def matchingUniverse : Finset (Parent (n := n)) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData.Parent
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.matching_potential_eq_card line 106
theorem OAI.LowSpaceSubsetSum.RepresentationParentData.collect_query_bounds line 128
Source documentation
Actual join reader calls, callbacks, snapshot copies, and outer control iterations are charged to raw child and matching occurrence counts.
```
theorem collect_query_bounds (B : ℕ) :
    let N := (D.pair 0).outputUniverse.card + (D.pair 1).outputUniverse.card
…
```