Internal: Nondeterministic Quantification Circuit Constructions

This internal module provides the circuit constructions needed for the nondeterministic quantification complexity bounds in Circ.Nondeterminism.

Circuit restriction

Given a circuit computing f : BitString ((k+1)+m) → Bool, we construct a circuit of the same size computing restrictFirst f b : BitString (k+m) → Bool (the function with its first input hardwired to b).

The key construction is restrictGateP, which transforms each gate in-place:

• If both inputs reference wire 0 (the hardwired input), the gate becomes a constant gate producing the correct value.
• If one input references wire 0, the gate simplifies to either a constant or an identity on the other input, depending on the operation and the hardwired value.
• If neither input references wire 0, both wire indices are shifted down by 1 (since the hardwired input is removed).

In all cases, the gate count is preserved.

OR combination

The OR of two Boolean functions has circuit complexity bounded by the sum of their complexities plus one, using ShannonUpper.binopCircuit.

Gate evaluation helpers

Restriction gate construction

def CircuitComplexity.mkConstGateP {k m G : ℕ} [NeZero m] (val : Bool) (bound : ℕ) : { g : Gate Basis.andOr2 (k + m + G) // ∀ (j : Fin g.fanIn), ↑(g.inputs j) < k + m + bound }

A constant-output gate: OR(x, ¬x) = true or AND(x, ¬x) = false.

Equations

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

def CircuitComplexity.mkIdentGateP {k m G : ℕ} (op : AONOp) (w : Fin (k + m + G)) (neg : Bool) (bound : ℕ) (hw : ↑w < k + m + bound) : { g : Gate Basis.andOr2 (k + m + G) // ∀ (j : Fin g.fanIn), ↑(g.inputs j) < k + m + bound }

An identity/passthrough gate: OP(w, w) with negation neg.

Equations

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

def CircuitComplexity.restrictGateP {k m G : ℕ} [NeZero m] (b : Bool) (g : Gate Basis.andOr2 (k + 1 + m + G)) (hfanIn : g.fanIn = 2) (bound : ℕ) (hbound : ∀ (j : Fin g.fanIn), ↑(g.inputs j) < k + 1 + m + bound) : { g' : Gate Basis.andOr2 (k + m + G) // ∀ (j : Fin g'.fanIn), ↑(g'.inputs j) < k + m + bound }

Transform a gate by hardwiring wire 0 to constant b.

The gate's two inputs are inspected. For each input referencing wire 0, the effective constant b ^^ negated is computed. The gate is then simplified: identity, constant, or shifted, depending on the case.

Equations

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

Restricted circuit

def CircuitComplexity.restrictCircuit {k m G : ℕ} [NeZero m] (b : Bool) (c : Circuit Basis.andOr2 (k + 1 + m) 1 G) : Circuit Basis.andOr2 (k + m) 1 G

The restricted circuit: same gate count, with each gate transformed by restrictGateP to account for the hardwired first input.

Equations

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

Correctness of restriction

theorem CircuitComplexity.restrictCircuit_eval {k m G : ℕ} [NeZero m] (b : Bool) (c : Circuit Basis.andOr2 (k + 1 + m) 1 G) (f : BitString (k + 1 + m) → Bool) (heval : (fun (x : BitString (k + 1 + m)) => c.eval x 0) = f) : (fun (x : BitString (k + m)) => (restrictCircuit b c).eval x 0) = restrictFirst f b

The restricted circuit computes restrictFirst f b.