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

Moving an affine gate into the affine system preserves the parameters of the state.

@[simp]

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

Moving an affine gate into the affine system preserves the pairs of the state.

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

Moving an affine gate into the affine system preserves the size of the state.

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

Moving an affine gate into the affine system decreases the number of gates by 1.

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

Rewiring a gate preserves the parameters of the state.

@[simp]

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

Rewiring a gate preserves the pairs of the state.

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

Rewiring a gate preserves the size of the state.

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

Rewiring a gate preserves the set of gate names.

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

A gate K is a child of z in S.rewire J g iff K ∈ S.gates and the gate at K (which is g when K = J) 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

Rewiring a gate preserves the equation children of every variable.

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.