Restrictions in the unbounded fan-in basis

A restriction (partial assignment) ρ of the inputs is computed in the unbounded fan-in basis by the De Morgan substitution circuit of ρ.toSubstitution (Cslib.Circuits.Boolean.substituteCircuit, Cslib.BitString.PartialAssignment.substitute_toSubstitution), its two constants becoming the conjunction and the disjunction of nothing (Cslib.Circuits.Boolean.Unbounded.deMorganToUnbounded). Composing a circuit C with it computes the restriction C ∘ ρ.fill.

Main definitions

• Cslib.Circuits.Boolean.Unbounded.restrictCircuit: the circuit outputting ρ.fill x.

Main results

• Cslib.Circuits.Boolean.Unbounded.eval_restrictCircuit, Cslib.Circuits.Boolean.Unbounded.size_restrictCircuit, Cslib.Circuits.Boolean.Unbounded.depth_restrictCircuit_le, Cslib.Circuits.Boolean.Unbounded.fanInAtMost_restrictCircuit: it computes ρ.fill with two gates, depth at most one and fan-in at most two.

def Cslib.Circuits.Boolean.Unbounded.restrictCircuit {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) : Circuit signature n n

The circuit that outputs its inputs restricted by ρ: the bits fixed by ρ replaced by their values (eval_restrictCircuit). It is the De Morgan substitution circuit of ρ.toSubstitution, in the unbounded fan-in basis.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.eval_restrictCircuit {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (x : BitString n) : (restrictCircuit ρ).eval interpretation x = ρ.fill x

restrictCircuit ρ computes ρ.fill.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.size_restrictCircuit {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) : (restrictCircuit ρ).size = 2

restrictCircuit ρ has two gates, one for each constant.

theorem Cslib.Circuits.Boolean.Unbounded.depth_restrictCircuit_le {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) : (restrictCircuit ρ).depth ≤ 1

restrictCircuit ρ has depth at most one.

theorem Cslib.Circuits.Boolean.Unbounded.fanInAtMost_restrictCircuit {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) : (restrictCircuit ρ).FanInAtMost 2

restrictCircuit ρ has fan-in at most two.