Derandomizing multi-output circuits

This module isolates the finite nonuniform randomness-fixing step for a randomized multi-output circuit. If the circuit fails its pointwise specification with probability at most 2^-(n + 1) on every n-bit input, then one seed works simultaneously on all inputs. Hardwiring that seed preserves the circuit's exact size.

This is the circuit-level union-bound step used when turning a sufficiently accurate randomized approximate counter into a deterministic nonuniform multi-output circuit.

def Complexity.Circuit.badSeedEvent {seedWidth inputWidth outputWidth internalGates : ℕ} [NeZero inputWidth] [NeZero outputWidth] (circuit : Circuit Basis.andOr2 (seedWidth + inputWidth) outputWidth internalGates) (IsCorrect : BitString inputWidth → BitString outputWidth → Prop) [(input : BitString inputWidth) → (output : BitString outputWidth) → Decidable (IsCorrect input output)] (input : BitString inputWidth) : Finset (BitString seedWidth)

The seeds on which a randomized circuit fails its output specification at one fixed input. Random bits occupy the circuit's input prefix.

Equations

• circuit.badSeedEvent IsCorrect input = {seed : Complexity.BitString seedWidth | ¬IsCorrect input (circuit.eval (Fin.append seed input))}

@[simp]

theorem Complexity.Circuit.mem_badSeedEvent_iff {seedWidth inputWidth outputWidth internalGates : ℕ} [NeZero inputWidth] [NeZero outputWidth] (circuit : Circuit Basis.andOr2 (seedWidth + inputWidth) outputWidth internalGates) (IsCorrect : BitString inputWidth → BitString outputWidth → Prop) [(input : BitString inputWidth) → (output : BitString outputWidth) → Decidable (IsCorrect input output)] (input : BitString inputWidth) (seed : BitString seedWidth) : seed ∈ circuit.badSeedEvent IsCorrect input ↔ ¬IsCorrect input (circuit.eval (Fin.append seed input))

Membership in the bad-seed event is exactly failure of the output specification on the seed-prefixed input.

theorem Complexity.Circuit.exists_uniform_correct_seed {seedWidth inputWidth outputWidth internalGates : ℕ} [NeZero inputWidth] [NeZero outputWidth] (circuit : Circuit Basis.andOr2 (seedWidth + inputWidth) outputWidth internalGates) (IsCorrect : BitString inputWidth → BitString outputWidth → Prop) [(input : BitString inputWidth) → (output : BitString outputWidth) → Decidable (IsCorrect input output)] (hfailure : ∀ (input : BitString inputWidth), eventProb (circuit.badSeedEvent IsCorrect input) ≤ 1 / 2 ^ (inputWidth + 1)) : ∃ (seed : BitString seedWidth), ∀ (input : BitString inputWidth), IsCorrect input (circuit.eval (Fin.append seed input))

A pointwise 2^-(n + 1) failure bound leaves one seed that satisfies a multi-output specification simultaneously on every n-bit input.

theorem Complexity.Circuit.exists_hardwired_correct_circuit {seedWidth inputWidth outputWidth internalGates : ℕ} [NeZero inputWidth] [NeZero outputWidth] (circuit : Circuit Basis.andOr2 (seedWidth + inputWidth) outputWidth internalGates) (IsCorrect : BitString inputWidth → BitString outputWidth → Prop) [(input : BitString inputWidth) → (output : BitString outputWidth) → Decidable (IsCorrect input output)] (hfailure : ∀ (input : BitString inputWidth), eventProb (circuit.badSeedEvent IsCorrect input) ≤ 1 / 2 ^ (inputWidth + 1)) : ∃ (fixed : Circuit Basis.andOr2 inputWidth outputWidth internalGates), (∀ (input : BitString inputWidth), IsCorrect input (fixed.eval input)) ∧ fixed.size = circuit.size

The uniformly correct seed can be hardwired without increasing circuit size, producing a deterministic multi-output circuit with the same pointwise specification.