Sparse separating filters

Hash the positive set into a shorter table, synthesize its image, and pull the result back along the hash. Every positive input survives; few specified negative inputs survive. Repeated filters reduce the remaining false positives geometrically.

theorem Complexity.CircuitSparseSynthesis.Internal.indicator_synthesis {n : ℕ} (s : Finset (BitString n)) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs n) {fun (x : BitString n) => decide (x ∈ s)} (s.card * (2 * n + 2) + 1)

theorem Complexity.CircuitSparseSynthesis.Internal.exists_sparse_filter {n k l : ℕ} (A B : Finset (BitString n)) (disjoint : Disjoint A B) (K : ℕ) (positive : 0 < K) : ∃ (f : BitString n → Bool), (∀ x ∈ B, f x = true) ∧ {x ∈ A | f x = true}.card * 2 ^ (k + l) ≤ A.card * B.card ∧ Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs n) {f} (hashBudget n (k + l) + sparseTableBudget k l K B.card)

theorem Complexity.CircuitSparseSynthesis.Internal.exists_repeated_filter {n k l p a : ℕ} (A B : Finset (BitString n)) (disjoint : Disjoint A B) (small : B.card ≤ 2 ^ p) (width : k + l = p + a) (K : ℕ) (positive : 0 < K) (steps : ℕ) : ∃ (f : BitString n → Bool), (∀ x ∈ B, f x = true) ∧ {x ∈ A | f x = true}.card * (2 ^ a) ^ steps ≤ A.card ∧ Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs n) {f} (steps * (hashBudget n (k + l) + sparseTableBudget k l K (2 ^ p) + 1) + 1)