Affine and quadratic reparameterisations

The reparameterisations (AR) and (QR) of Mishra and Santhanam, Section 3.2 on states of gate elimination. Both change the parameters bijectively, so the image of the parameter map is unchanged:

• State.swap: an unpaired parameter x and an auxiliary variable Q depending on it exchange their roles, and the parameter map substitutes x = Q + c + ∑ j ∈ T \ {x}, u j; no equation or gate changes (State.Valid.swap);
• State.quad: for an AND-type gate G = (x + α)(y + β) + γ whose only child is the XOR-type gate D = G + z + c reading an isolated parameter z, the parameter map substitutes z = D + G + c, the gate D becomes a parameter, G and D are deleted and x is paired with y (State.Valid.quad).

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.swap, Cslib.Circuits.Boolean.AffineDisperser.State.SwapOK, Cslib.Circuits.Boolean.AffineDisperser.State.quad, Cslib.Circuits.Boolean.AffineDisperser.State.QuadOK: the reparameterisations and their hypotheses.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.swap, Cslib.Circuits.Boolean.AffineDisperser.State.Valid.quad: they preserve validity.

References

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

Affine reparameterisation (AR)

def Cslib.Circuits.Boolean.AffineDisperser.State.swap {n : ℕ} (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : State n

Exchange the parameter x with the auxiliary variable Q = c + ∑ j ∈ T, u j depending on it: Q becomes a parameter, x an auxiliary variable, and the parameter map substitutes x = Q + c + ∑ j ∈ T \ {x}, u j. No equation or gate changes.

structure Cslib.Circuits.Boolean.AffineDisperser.State.SwapOK {n : ℕ} (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : Prop

The hypotheses of the affine reparameterisation.

• mem : x ∈ S.params
• unpaired : ¬S.Paired x
• aux : Q ∈ S.aux
• affine : SemiCircuit.AffineIn Q c T
• mem_T : x ∈ T

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.swap_params {n : ℕ} (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : (S.swap x Q c T).params = insert Q (S.params.erase x)

Exchanging x and Q replaces x with Q in S.params.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.swap_pairs {n : ℕ} (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : (S.swap x Q c T).pairs = S.pairs

Exchanging x and Q preserves the pairs of the state.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.swap_size {n : ℕ} (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : (S.swap x Q c T).size = S.size

Exchanging x and Q preserves the size of the state.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.swap_children {n : ℕ} (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) (z : ℕ) : (S.swap x Q c T).children z = S.children z

Exchanging x and Q preserves the children of every variable.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.swap {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x Q : ℕ} {c : Bool} {T : Finset ℕ} (h : S.SwapOK x Q c T) : (S.swap x Q c T).Valid f

The affine reparameterisation preserves validity.

Quadratic reparameterisation (QR)

def Cslib.Circuits.Boolean.AffineDisperser.State.quad {n : ℕ} (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : State n

The quadratic reparameterisation: for an AND-type gate G = (x + α)(y + β) + γ whose only child is the XOR-type gate D = G + z + c, where z is an isolated parameter, substitute z = D + G + c in the parameter map, turn D into a parameter (it computes the new parameter w of the source), delete the gates G and D, and pair x with y.

structure Cslib.Circuits.Boolean.AffineDisperser.State.QuadOK {n : ℕ} (S : State n) (x y z G D : ℕ) (α β γ c : Bool) extends S.QuadOK x y z G D α β γ c : Prop

The hypotheses of the quadratic reparameterisation: the configuration of SemiCircuit.QuadOK on unpaired parameters.

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

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.quad_params {n : ℕ} (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : (S.quad x y z G D α β γ c).params = insert D (S.params.erase z)

The quadratic reparameterisation replaces z with D in S.params.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.quad_pairs {n : ℕ} (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : (S.quad x y z G D α β γ c).pairs = insert (x, y) S.pairs

The quadratic reparameterisation inserts (x, y) into S.pairs.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.quad_size {n : ℕ} {S : State n} {x y z G D : ℕ} {α β γ c : Bool} (h : S.QuadOK x y z G D α β γ c) : (S.quad x y z G D α β γ c).size + 2 = S.size

The quadratic reparameterisation decreases the size of the state by 2.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.quad_children_subset {n : ℕ} (S : State n) (x y z G D : ℕ) (α β γ c : Bool) (w : ℕ) : (S.quad x y z G D α β γ c).children w ⊆ ((S.children w).erase (Sum.inl D)).erase (Sum.inl G)

After the quadratic reparameterisation, the children of w are contained in S.children w with .inl D and .inl G removed.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.QuadOK.pair_mem {n : ℕ} {f : BooleanFunction n} {S : State n} {x y z G D : ℕ} {α β γ c : Bool} (h : S.QuadOK x y z G D α β γ c) (hS : S.Valid f) (pr : ℕ × ℕ) : pr ∈ (S.quad x y z G D α β γ c).pairs → pr.1 ∈ (S.quad x y z G D α β γ c).params ∧ pr.2 ∈ (S.quad x y z G D α β γ c).params ∧ pr.1 ≠ pr.2

The pairs after the quadratic reparameterisation are disjoint pairs of parameters.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.quad {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool} (h : S.QuadOK x y z G D α β γ c) : (S.quad x y z G D α β γ c).Valid f

The quadratic reparameterisation preserves validity.