The semi-circuit of a circuit

A circuit over the full binary basis with n inputs and one output is a fair semi-circuit without equations (SemiCircuit.ofCircuit): input i is the parameter i, gate j is the gate n + j, and a constant line becomes a gate with a constant operation. It is well formed (SemiCircuit.wellFormed_ofCircuit), and the output of a consistent assignment is the output of the circuit on the values of the parameters (SemiCircuit.out_eval_ofCircuit).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit.ofCircuit: the semi-circuit of a circuit.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.wellFormed_ofCircuit, Cslib.Circuits.Boolean.SemiCircuit.out_eval_ofCircuit.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits

def Cslib.Circuits.Boolean.SemiCircuit.wireName {n g : ℕ} : Wire n g → ℕ

The name of a wire of a circuit with n inputs: input i is i and gate j is n + j.

def Cslib.Circuits.Boolean.SemiCircuit.lineGate {n g : ℕ} : Line (fullSignature 2 Bool) n g → Gate

The gate of a line of a circuit over the full binary basis; a constant becomes a gate with a constant operation.

theorem Cslib.Circuits.Boolean.SemiCircuit.eval_lineGate {n g : ℕ} (line : Line (fullSignature 2 Bool) n g) (val : ℕ → Bool) : (lineGate line).eval val = fullInterpretation line.op fun (a : Fin ((fullSignature 2 Bool).Arity line.op)) => val (wireName (line.wires a))

theorem Cslib.Circuits.Boolean.SemiCircuit.reads_lineGate {n g : ℕ} {line : Line (fullSignature 2 Bool) n g} {i : ℕ} (h : (lineGate line).Reads i) : ∃ (a : Fin ((fullSignature 2 Bool).Arity line.op)), wireName (line.wires a) = i

def Cslib.Circuits.Boolean.SemiCircuit.ofCircuit {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : SemiCircuit

The semi-circuit of a circuit over the full binary basis with one output: its inputs are the parameters, its lines the gates, and it has no auxiliary variables and no equations.

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_params {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).params = Finset.range n

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_aux {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).aux = ∅

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_gates {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).gates = Finset.Ico n (n + C.size)

@[simp]

theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_eqns {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).eqns = ∅

theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_gate {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) (k : Fin C.size) : (ofCircuit C).gate (n + ↑k) = lineGate (C.program.lines k)

theorem Cslib.Circuits.Boolean.SemiCircuit.wireName_mem_live {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) (w : Wire n C.size) : wireName w ∈ (ofCircuit C).live

theorem Cslib.Circuits.Boolean.SemiCircuit.exists_eq_add_of_mem_gates {n : ℕ} {C : Circuit (fullSignature 2 Bool) n 1} {J : ℕ} (hJ : J ∈ (ofCircuit C).gates) : ∃ (k : Fin C.size), J = n + ↑k

theorem Cslib.Circuits.Boolean.SemiCircuit.wellFormed_ofCircuit {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (ofCircuit C).WellFormed

The semi-circuit of a circuit is well formed.

theorem Cslib.Circuits.Boolean.SemiCircuit.out_eval_ofCircuit {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) {val : ℕ → Bool} (hval : (ofCircuit C).Consistent val) : (ofCircuit C).out.eval val = C.eval fullInterpretation (fun (i : Fin n) => val ↑i) 0

On a consistent assignment, the output of the semi-circuit of a circuit is the output of the circuit on the values of the parameters.