Exchanging parameters

Two changes of the parameters of a fair semi-circuit, the semi-circuit side of the reparameterisations (AR) and (QR) of Mishra and Santhanam, Section 3.2:

• SemiCircuit.swap: a parameter x and an auxiliary variable Q depending on it exchange their roles; no gate or equation changes, and well-formedness is preserved (WellFormed.swap), since on the solutions of the affine system x is determined by Q and the other parameters (AffineIn.solve);
• SemiCircuit.quad: for an AND-type gate G whose only child is the XOR-type gate D = G + z + c reading an isolated parameter z, the gate D becomes a parameter in place of z and both gates are deleted (WellFormed.quad); a consistent assignment of the result, with z and G given their values, is consistent for the original semi-circuit (QuadOK.consistent).

Main definitions

• Cslib.Circuits.Boolean.SemiCircuit.swap, Cslib.Circuits.Boolean.SemiCircuit.quad.

Main results

• Cslib.Circuits.Boolean.SemiCircuit.WellFormed.swap, Cslib.Circuits.Boolean.SemiCircuit.WellFormed.quad: well-formedness is preserved.

References

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

Exchanging a parameter and an auxiliary variable

def Cslib.Circuits.Boolean.SemiCircuit.swap (C : SemiCircuit) (x Q : ℕ) : SemiCircuit

Exchange the parameter x with the auxiliary variable Q. No equation or gate changes.

theorem Cslib.Circuits.Boolean.SemiCircuit.AffineIn.solve {C : SemiCircuit} {Q x : ℕ} {c : Bool} {T : Finset ℕ} (h : AffineIn Q c T) (hxT : x ∈ T) {val : ℕ → Bool} (hval : C.EqnsHold val) : val x = val Q + c + ∑ j ∈ T.erase x, val j

On the solutions of the affine system, a parameter x on which Q = c + ∑ j ∈ T, u j depends is Q + c + ∑ j ∈ T \ {x}, u j.

theorem Cslib.Circuits.Boolean.SemiCircuit.params_union_aux_swap {C : SemiCircuit} {x Q : ℕ} (hx : x ∈ C.params) (hQ : Q ∈ C.aux) : (C.swap x Q).params ∪ (C.swap x Q).aux = C.params ∪ C.aux

theorem Cslib.Circuits.Boolean.SemiCircuit.live_swap {C : SemiCircuit} {x Q : ℕ} (hx : x ∈ C.params) (hQ : Q ∈ C.aux) : (C.swap x Q).live = C.live

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.swap {C : SemiCircuit} (hC : C.WellFormed) {x Q : ℕ} {c : Bool} {T : Finset ℕ} (hx : x ∈ C.params) (hQ : Q ∈ C.aux) (haff : AffineIn Q c T) (hxT : x ∈ T) : (C.swap x Q).WellFormed

Exchanging a parameter x with an auxiliary variable depending on it preserves well-formedness.

The quadratic reparameterisation

def Cslib.Circuits.Boolean.SemiCircuit.quad (C : SemiCircuit) (z G D : ℕ) : SemiCircuit

Turn the gate D into a parameter in place of z, and delete the gates G and D.

theorem Cslib.Circuits.Boolean.SemiCircuit.mem_live_quad {C : SemiCircuit} {z G D i : ℕ} (hi : i ∈ C.live) (hiz : i ≠ z) (hiG : i ≠ G) : i ∈ (C.quad z G D).live

structure Cslib.Circuits.Boolean.SemiCircuit.QuadOK (C : SemiCircuit) (x y z G D : ℕ) (α β γ c : Bool) : Prop

The configuration of the quadratic reparameterisation: an AND-type gate G = (x + α)(y + β) + γ on the distinct parameters x and y, whose only child is the XOR-type gate D = G + z + c, where D is the only child of the parameter z, and neither G nor z is the output.

• mem_x : x ∈ C.params
• mem_y : y ∈ C.params
• mem_z : z ∈ C.params
• x_ne_y : x ≠ y
• x_ne_z : x ≠ z
• y_ne_z : y ≠ z
• mem_G : G ∈ C.gates
• mem_D : D ∈ C.gates
• G_ne_D : G ≠ D
• eval_G (val : ℕ → Bool) : (C.gate G).eval val = (val x + α) * (val y + β) + γ
• eval_D (val : ℕ → Bool) : (C.gate D).eval val = val G + val z + c
• children_G : C.children G = {Sum.inl D}
• children_z : C.children z = {Sum.inl D}
• out_G : ¬C.out.Reads G
• out_z : ¬C.out.Reads z

theorem Cslib.Circuits.Boolean.SemiCircuit.QuadOK.notMem_terms_z {C : SemiCircuit} {x y z G D : ℕ} {α β γ c : Bool} (h : C.QuadOK x y z G D α β γ c) {e : ℕ} (he : e ∈ C.eqns) : z ∉ (C.eqn e).terms

theorem Cslib.Circuits.Boolean.SemiCircuit.QuadOK.not_reads_z {C : SemiCircuit} {x y z G D : ℕ} {α β γ c : Bool} (h : C.QuadOK x y z G D α β γ c) {K : ℕ} (hK : K ∈ C.gates) (hKD : K ≠ D) : ¬(C.gate K).Reads z

theorem Cslib.Circuits.Boolean.SemiCircuit.QuadOK.not_reads_G {C : SemiCircuit} {x y z G D : ℕ} {α β γ c : Bool} (h : C.QuadOK x y z G D α β γ c) {K : ℕ} (hK : K ∈ C.gates) (hKD : K ≠ D) : ¬(C.gate K).Reads G

theorem Cslib.Circuits.Boolean.SemiCircuit.WellFormed.quad {C : SemiCircuit} (hC : C.WellFormed) {x y z G D : ℕ} {α β γ c : Bool} (h : C.QuadOK x y z G D α β γ c) : (C.quad z G D).WellFormed

The quadratic reparameterisation preserves well-formedness.

def Cslib.Circuits.Boolean.SemiCircuit.quadValue (x y z G D : ℕ) (α β γ c : Bool) (val : ℕ → Bool) : ℕ → Bool

The assignment of the original semi-circuit determined by an assignment of its quadratic reparameterisation: z = D + G + c and G takes its value.

theorem Cslib.Circuits.Boolean.SemiCircuit.QuadOK.consistent {C : SemiCircuit} (hC : C.WellFormed) {x y z G D : ℕ} {α β γ c : Bool} (h : C.QuadOK x y z G D α β γ c) {val : ℕ → Bool} (hval : (C.quad z G D).Consistent val) : C.Consistent (quadValue x y z G D α β γ c val) ∧ (C.quad z G D).out.eval val = C.out.eval (quadValue x y z G D α β γ c val)

A consistent assignment of the quadratic reparameterisation gives a consistent assignment of the original semi-circuit with the same output.