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.quad: the reparameterisations.

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)

@[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

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

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

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)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.isAffine_mul_of_pairTame {k : ℕ} {τ : BitString k → ℕ → Bool} (hτ : BitString.IsAffine τ) {x y : ℕ} (ht : PairTame τ (x, y)) (α β : Bool) : BitString.IsAffine fun (u : BitString k) => (τ u x + α) * (τ u y + β)

Along an affine family on which the pair (x, y) is tame, the product (u x + α) (u y + β) is affine.

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)

@[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

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

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)

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.QuadOK.pairs_disjoint {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' ∈ (S.quad x y z G D α β γ c).pairs, pr ≠ pr' → pr.1 ≠ pr'.1 ∧ pr.1 ≠ pr'.2 ∧ pr.2 ≠ pr'.1 ∧ pr.2 ≠ pr'.2

theorem Cslib.Circuits.Boolean.AffineDisperser.State.QuadOK.affine {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) {k : ℕ} {τ : BitString k → ℕ → Bool} (hτ : BitString.IsAffine τ) (htame : ∀ pr ∈ (S.quad x y z G D α β γ c).pairs, PairTame τ pr) : ∃ (τ' : BitString k → ℕ → Bool), BitString.IsAffine τ' ∧ (∀ pr ∈ S.pairs, PairTame τ' pr) ∧ ∀ (u : BitString k), ∀ j ∈ S.params, τ' u j = SemiCircuit.quadValue x y z G D α β γ c (τ u) j

Along an affine family on which the new pairs are tame, substituting z keeps it affine and every old pair tame: the new pair (x, y) makes the product G affine.

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.