Fixing the random seed of a circuit with several outputs

A randomized circuit reads an input x of n bits followed by a seed r of p bits, and its outputs should satisfy a specification Correct x that may allow several answers, as for an approximate count. If, at every input, fewer than a 2 ^ (-n) fraction of the seeds make it fail, then by the union bound over the 2 ^ n inputs some seed makes it correct at every input at once (Circuit.exists_seed_forall). Hardwiring that seed costs two gates for the constants and one level of depth (Boolean.exists_circuit_of_card_bad_lt). This is the nonuniform derandomization of Adleman's theorem without amplification Arora and Barak, Theorem 7.14, [Adl78], for circuits with any number of outputs.

Main results

• Cslib.Circuits.Circuit.exists_seed_forall: a seed that is good for every input, over any basis.
• Cslib.Circuits.Boolean.exists_circuit_of_card_bad_lt: a deterministic De Morgan circuit with the seed hardwired.
• Cslib.Circuits.Boolean.exists_computes_of_card_bad_lt: the same when the specification is a function.

This recovers the earlier Complexitylib Classes/Randomized/CircuitHardwiring formalization by Samuel Schlesinger, using the current shared-constant substitution circuit.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 7.5
• L. Adleman, Two theorems on random polynomial time

theorem Cslib.Circuits.Circuit.exists_seed_forall {n p m : ℕ} {σ : Signature} {I : Interpretation σ Bool} (C : Circuit σ (n + p) m) (Correct : BitString n → BitString m → Prop) [(x : BitString n) → (y : BitString m) → Decidable (Correct x y)] (h : ∀ (x : BitString n), 2 ^ n * {r : BitString p | ¬Correct x (C.eval I (Fin.append x r))}.card < 2 ^ p) : ∃ (r : BitString p), ∀ (x : BitString n), Correct x (C.eval I (Fin.append x r))

A seed good for every input. If, at every input x of n bits, fewer than a 2 ^ (-n) fraction of the seeds r make the outputs on x ++ r violate Correct x, then one seed makes them satisfy it at every input.

theorem Cslib.Circuits.Boolean.exists_circuit_of_card_bad_lt {n p m : ℕ} (C : Circuit signature (n + p) m) (Correct : BitString n → BitString m → Prop) [(x : BitString n) → (y : BitString m) → Decidable (Correct x y)] (h : ∀ (x : BitString n), 2 ^ n * {r : BitString p | ¬Correct x (C.eval interpretation (Fin.append x r))}.card < 2 ^ p) : ∃ (D : Circuit signature n m), (∀ (x : BitString n), Correct x (D.eval interpretation x)) ∧ D.size ≤ C.size + 2 ∧ D.depth ≤ C.depth + 1

Fixing the seed of a De Morgan circuit. If, at every input x of n bits, fewer than a 2 ^ (-n) fraction of the seeds r make the outputs on x ++ r violate Correct x, then a deterministic circuit with at most two more gates, and at most one more level, satisfies Correct x at every input.

theorem Cslib.Circuits.Boolean.exists_computes_of_card_bad_lt {n p m : ℕ} (C : Circuit signature (n + p) m) (f : BitString n → BitString m) (h : ∀ (x : Fin n → Bool), 2 ^ n * {r : BitString p | C.eval interpretation (Fin.append x r) ≠ f x}.card < 2 ^ p) : ∃ (D : Circuit signature n m), D.Computes interpretation f ∧ D.size ≤ C.size + 2 ∧ D.depth ≤ C.depth + 1

Fixing the seed of a De Morgan circuit computing a function. If, at every input x of n bits, the outputs on x ++ r differ from f x for fewer than a 2 ^ (-n) fraction of the seeds r, then a deterministic circuit with at most two more gates, and at most one more level, computes f.