Deletions in gate elimination

Case 1 of the preliminary reductions of Mishra and Santhanam, Section 4.1 (State.DeletionAvailable): one of the deletions (D1)–(D4) applies, lowering s, keeping a and not increasing W (State.Valid.step_of_deletion).

• (D1) a gate computing, on the solutions of the affine system, a constant or a literal of one of its inputs is deleted, and (D2) so is a gate other than the output with no children; both are State.Reductions through State.reduction_deleteGate.
• (D3) an equation with at most two terms is deleted (State.Valid.exists_reduction_delete).
• (D4) an unpaired parameter whose only child is an equation is exchanged with an auxiliary variable of that equation, which is then dropped (State.Valid.unit_delete). This changes the parameters, so it is not a State.Reduction; its accounting is done directly.

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.DeletionAvailable: the configuration of Case 1.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.unit_delete: the deletion (D4).
• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_deletion: a deletion is a step of gate elimination.

References

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

theorem Cslib.Circuits.Boolean.AffineDisperser.State.children_eq_singleton {n : ℕ} {S : State n} {p : ℕ} {H : ℕ ⊕ ℕ} (h1 : S.deg p = 1) (hH : H ∈ S.children p) : S.children p = {H}

def Cslib.Circuits.Boolean.AffineDisperser.State.DeletionAvailable {n : ℕ} (S : State n) : Prop

The configuration of Case 1: one of the deletions (D1)–(D4) applies. An equation has at most two terms (D3); a gate computes, on the solutions of the affine system, a constant or a literal of one of its inputs (D1); a gate other than the output has no children (D2); or an unpaired parameter has an equation as its only child (D4).

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.not_out_reads_param {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) {x : ℕ} (hx : x ∈ S.params) : ¬S.out.Reads x

In a valid state with d < a, the output is not a literal of a parameter, by Lemma 2.3.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.unit_delete {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) {x e : ℕ} (hx : x ∈ S.unpaired) (hc : S.children x = {Sum.inr e}) : ∃ (S' : State n), S'.Valid f ∧ S'.m = S.m ∧ S'.s + 1 = S.s ∧ S'.a = S.a ∧ S'.q = S.q ∧ S'.W + 1 ≤ S.W

(D4): an unpaired parameter x whose only child is the equation e is exchanged with an auxiliary variable depending on it and then deleted with e; this keeps a and lowers W.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_unit {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) {x e : ℕ} (hx : x ∈ S.unpaired) (hc : S.children x = {Sum.inr e}) : ∃ (S' : State n), Step f S S'

(D4) as a step of gate elimination.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.card_filter_inl_mem_children_le {n : ℕ} (S : State n) (J : ℕ) : {u ∈ S.params | Sum.inl J ∈ S.children u}.card ≤ 2

A gate has at most two parameters as parents.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_deletion {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (h : S.DeletionAvailable) : ∃ (S' : State n), Step f S S'

Case 1 of the preliminary reductions: a deletion lowers s, keeps a and does not increase W.