Partial synthesis after hashing

Choose a representative label for every occupied hash cell, synthesize the resulting short partial table, and patch the input points whose labels were lost in collisions. Pairwise independence bounds this last cost.

def Complexity.CircuitSparseSynthesis.Internal.partialFiniteBudget (n k l K weight : ℕ) : ℕ

Hash cost, partial-table cost, collision repairs by minterms, and a final XOR.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.CircuitSparseSynthesis.Internal.exists_partialFinite {n k l : ℕ} (domain : Finset (BitString n)) (f : BitString n → Bool) (K : ℕ) (positive : 0 < K) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature n 1), (c.ComputesOn Cslib.Circuits.Boolean.interpretation ↑domain fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.size ≤ partialFiniteBudget n k l K domain.card