Moving and rewiring gates of states

The preparatory operations of Mishra and Santhanam, Sections 4.1 and 4.2 that change only gates, on states of gate elimination:

• State.moveAffine: moving an affine gate reading no gates into the affine system, as the equation SemiCircuit.affEqn (State.Valid.moveAffine);
• State.rewire: replacing a gate by one reading only parameters and computing the same value whenever the other gates take their values, used to reroute the children of the minimal AND (State.Valid.rewire).

Both keep the parameters, the pairs and the parameter map.

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine, Cslib.Circuits.Boolean.AffineDisperser.State.rewire.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.moveAffine, Cslib.Circuits.Boolean.AffineDisperser.State.Valid.rewire: they preserve validity.

References

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

Moving affine gates into the affine system

def Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine {n : ℕ} (S : State n) (J e : ℕ) : State n

Move the affine gate J into the affine system as the auxiliary variable J with the new equation e.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine_params {n : ℕ} (S : State n) (J e : ℕ) : (S.moveAffine J e).params = S.params

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine_pairs {n : ℕ} (S : State n) (J e : ℕ) : (S.moveAffine J e).pairs = S.pairs

theorem Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine_size {n : ℕ} {S : State n} {J e : ℕ} (h : S.MoveOK J e) : (S.moveAffine J e).size = S.size

theorem Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine_gates_card {n : ℕ} {S : State n} {J e : ℕ} (h : S.MoveOK J e) : (S.moveAffine J e).gates.card + 1 = S.gates.card

theorem Cslib.Circuits.Boolean.AffineDisperser.State.moveAffine_deg_le {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J e : ℕ} (h : S.MoveOK J e) {z : ℕ} (hz : z ∈ S.params) : (S.moveAffine J e).deg z ≤ S.deg z

Moving a gate into the affine system does not increase the degree of any parameter.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.moveAffine {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J e : ℕ} (h : S.MoveOK J e) : (S.moveAffine J e).Valid f

Moving an affine gate reading no gates into the affine system preserves validity.

Rewiring a gate

def Cslib.Circuits.Boolean.AffineDisperser.State.rewire {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) : State n

Replace the gate J by the gate g.

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.rewire_params {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) : (S.rewire J g).params = S.params

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.rewire_pairs {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) : (S.rewire J g).pairs = S.pairs

theorem Cslib.Circuits.Boolean.AffineDisperser.State.rewire_size {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) : (S.rewire J g).size = S.size

theorem Cslib.Circuits.Boolean.AffineDisperser.State.rewire_gates {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) : (S.rewire J g).gates = S.gates

theorem Cslib.Circuits.Boolean.AffineDisperser.State.inl_mem_children_rewire {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) (z K : ℕ) : Sum.inl K ∈ (S.rewire J g).children z ↔ K ∈ S.gates ∧ if K = J then g.Reads z else (S.gate K).Reads z

theorem Cslib.Circuits.Boolean.AffineDisperser.State.inr_mem_children_rewire {n : ℕ} (S : State n) (J : ℕ) (g : SemiCircuit.Gate) (z e : ℕ) : Sum.inr e ∈ (S.rewire J g).children z ↔ Sum.inr e ∈ S.children z

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.rewire {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} {g : SemiCircuit.Gate} (h : S.RewireOK J g) : (S.rewire J g).Valid f

Rewiring a gate preserves validity.