Reductions and their accounting

Every reduction of the gate elimination of Mishra and Santhanam, Section 4 restricts some parameters and then deletes some gates and equations. A reduction (State.Reduction f S S' F D T) from S to S' restricts the parameters of F, each to a constant or to a literal of a remaining parameter with at least its children, drops the pairs meeting F, and then deletes the constraints of the list D. Only the deletions of the constraints of T may reroute a constraint to a parameter; the others reroute to constants or to non-parameters. Reductions compose (State.Reduction.trans), and are built from restrictions (State.Valid.reduction_restrict, State.Valid.reduction_fixConst) and deletions (State.Valid.reduction_deleteGate, State.Valid.reduction_deleteEqn, State.Valid.exists_reduction_deleteAll).

The accounting is done once for all reductions:

• Δm = -|F|, Δs = -|D| and Δq = -k, where k is the number of pairs meeting F (State.Reduction.m_add, State.Reduction.s_add, State.Reduction.q_add);
• the unpaired parameters of S' are those of S outside F, together with the partners of members of F (State.Reduction.mem_unpaired_iff);
• a parameter that no deletion of T reroutes to keeps at most its children outside D (State.Reduction.wt_le_weight), and an unpaired parameter rerouted to only by deletions of constraints with another parameter as a parent does not gain weight in an exclusive state (State.Reduction.wt_le_of_exclusive);
• the potential: W' + 2 |D| + 3 k + ∑_{x ∈ F} wt(x) ≤ W plus the pointwise gains (State.Reduction.W_le), and a reduction restricting at most two parameters with W' + 14 |F| ≤ W + 14 k is a step of gate elimination (State.Reduction.step).

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.Reduction: reductions.
• Cslib.Circuits.Boolean.AffineDisperser.State.Deletable: constraints deletable by (D1) or (D3).
• Cslib.Circuits.Boolean.AffineDisperser.State.Exclusive: no constraint has an unpaired isolated parameter and another parameter as parents.
• Cslib.Circuits.Boolean.AffineDisperser.State.fixConst: fixing a parameter to a constant.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.W_le: the potential of a reduction.
• Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.step: reductions as steps of gate elimination.
• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_deleteAll: deleting deletable constraints.

References

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

Exclusive states

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

No constraint has both an unpaired isolated parameter and another parameter as parents.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Exclusive.two_le_deg {n : ℕ} {S : State n} (h : S.Exclusive) {u x : ℕ} {N : ℕ ⊕ ℕ} (hu : u ∈ S.unpaired) (hNu : N ∈ S.children u) (hx : x ∈ S.params) (hxu : x ≠ u) (hNx : N ∈ S.children x) : 2 ≤ S.deg u

In an exclusive state, an unpaired parameter sharing a child with another parameter has degree at least two.

Deletable constraints

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

A deletable constraint: a gate with a constant argument or two equal arguments, or an equation with at most two terms.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletable_fixConst_child {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {p : ℕ} (P : Finset (ℕ × ℕ)) (b : Bool) {N : ℕ ⊕ ℕ} (hN : N ∈ S.children p) : (S.restrict p (SemiCircuit.Lit.const b) P).Deletable N

The children of a parameter fixed to a constant are deletable.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletable_deleteGate_child {n : ℕ} {S : State n} {J K : ℕ} (c : Bool) (hK : K ∈ S.gates) (hKJ : K ≠ J) (hr : (S.gate K).Reads J) : (S.deleteGate J (SemiCircuit.Lit.const c)).Deletable (Sum.inl K)

After deleting the gate J rerouted to a constant, the gates reading J are deletable.

Reductions

structure Cslib.Circuits.Boolean.AffineDisperser.State.Reduction {n : ℕ} (f : BooleanFunction n) (S S' : State n) (F : Finset ℕ) (D T : List (ℕ ⊕ ℕ)) : Prop

A reduction from S to S': the parameters of F are restricted, each to a constant or to a literal of a remaining parameter having at least its children, the pairs meeting F are dropped, and the constraints of D are deleted. The children of a remaining parameter lose the deleted constraints and gain none, unless a deletion of a constraint of T that was one of its children reroutes to it; and the other constraints stay deletable.

• valid : S'.Valid f

  The new state is valid.

• subset : F ⊆ S.params

  The restricted names are parameters.

• params : S'.params = S.params \ F

  The restricted parameters are removed.

• pairs : S'.pairs = {pr ∈ S.pairs | ¬(pr.1 ∈ F ∨ pr.2 ∈ F)}

  The pairs meeting the restricted parameters are dropped.

• size : S'.size + D.length = S.size

  The deleted constraints are removed.

• children (u : ℕ) : u ∈ S'.params → S'.children u ⊆ S.children u \ D.toFinset ∨ ∃ N ∈ T, N ∈ S.children u

  A remaining parameter gains no child, unless a deletion of T reroutes to it.

• deletable (N : ℕ ⊕ ℕ) : N ∉ D → S.Deletable N → S'.Deletable N

  The other constraints stay deletable.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.refl {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) : Reduction f S S ∅ [] []

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.trans {n : ℕ} {f : BooleanFunction n} {S S₁ S₂ : State n} {F₁ F₂ : Finset ℕ} {D₁ D₂ T₁ T₂ : List (ℕ ⊕ ℕ)} (h₁ : Reduction f S S₁ F₁ D₁ T₁) (h₂ : Reduction f S₁ S₂ F₂ D₂ T₂) : Reduction f S S₂ (F₁ ∪ F₂) (D₁ ++ D₂) (T₁ ++ T₂)

Reductions compose.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.trans_delete {n : ℕ} {f : BooleanFunction n} {S : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} {S₁ S₂ : State n} {D₂ T₂ : List (ℕ ⊕ ℕ)} (h₁ : Reduction f S S₁ F D T) (h₂ : Reduction f S₁ S₂ ∅ D₂ T₂) : Reduction f S S₂ F (D ++ D₂) (T ++ T₂)

A reduction followed by a reduction restricting nothing.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.mono {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) {T' : List (ℕ ⊕ ℕ)} (hT : ∀ N ∈ T, N ∈ T') : Reduction f S S' F D T'

A reduction may record more deletions as possibly rerouting to parameters.

Accounting

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.m_add {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) : S'.m + F.card = S.m

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.s_add {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) : S'.s + D.length = S.s

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.q_add {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) : S'.q + (S.pairsMeeting F).card = S.q

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.a_add {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) : S'.a + F.card = S.a + (S.pairsMeeting F).card

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.mem_unpaired_iff {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) {u : ℕ} : u ∈ S'.unpaired ↔ u ∈ S.params ∧ u ∉ F ∧ (¬S.Paired u ∨ ∃ x ∈ F, S.IsPartner x u)

The unpaired parameters after a reduction: the unpaired parameters outside F and the partners of members of F.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_eq_zero {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) {u : ℕ} (hu : u ∉ S.unpaired) (hpart : ∀ x ∈ F, ¬S.IsPartner x u) : S'.wt u = 0

A paired parameter that is not the partner of a member of F stays paired.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_le_weight {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) {u : ℕ} (hT : ∀ N ∈ T, N ∉ S.children u) : S'.wt u ≤ weight (S.children u \ D.toFinset).card

A parameter that no deletion of T reroutes to keeps at most its children outside D.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.children_subset {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) {u : ℕ} (hu : u ∈ S'.params) (hT : ∀ N ∈ T, N ∉ S.children u) : S'.children u ⊆ S.children u \ D.toFinset

A parameter that no deletion of T reroutes to keeps at most its children outside D.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_le {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) {u : ℕ} (hpart : ∀ x ∈ F, ¬S.IsPartner x u) (hT : ∀ N ∈ T, N ∉ S.children u) : S'.wt u ≤ S.wt u

A parameter that is not the partner of a member of F, and that no deletion reroutes to, does not gain weight.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_le_add_one {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) {u : ℕ} (hpart : ∀ x ∈ F, ¬S.IsPartner x u) (hdeg : 1 ≤ S.deg u) : S'.wt u ≤ S.wt u + 1

A used parameter that is not the partner of a member of F gains at most one in weight.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_eq_zero_of_subset {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) {u : ℕ} (hsub : S.children u ⊆ D.toFinset) (hT : ∀ N ∈ T, N ∉ S.children u) : S'.wt u = 0

A parameter all of whose children are deleted, and that no deletion reroutes to, becomes unused.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_le_wt {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) {u : ℕ} (hu : u ∈ S.unpaired) (hT : ∀ N ∈ T, N ∈ S.children u → 2 ≤ S.deg u) : S'.wt u ≤ S.wt u

An unpaired parameter does not gain weight when it has degree at least two if some deletion may reroute to it.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_le_of_exclusive {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) (hexcl : S.Exclusive) {u : ℕ} (hpart : ∀ x ∈ F, ¬S.IsPartner x u) (hT : ∀ N ∈ T, N ∈ S.children u → ∃ x ∈ S.params, x ≠ u ∧ N ∈ S.children x) : S'.wt u ≤ S.wt u

In an exclusive state, a parameter that is not the partner of a member of F does not gain weight when every deletion that may reroute to it deletes a constraint with another parameter as a parent.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.W_le {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (loss gain : ℕ → ℕ) (hpt : ∀ u ∈ S.params \ F, S'.wt u + loss u ≤ S.wt u + gain u) : S'.W + 2 * D.length + 3 * (S.pairsMeeting F).card + ∑ u ∈ F, S.wt u + ∑ u ∈ S.params \ F, loss u ≤ S.W + ∑ u ∈ S.params \ F, gain u

The potential of a reduction. If every parameter outside F gains at most gain and loses at least loss in weight, then W' + 2 |D| + 3 k + ∑_{x ∈ F} wt(x) + ∑ loss ≤ W + ∑ gain, where k is the number of pairs meeting F.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.step {n : ℕ} {f : BooleanFunction n} {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)} (h : Reduction f S S' F D T) (hS : S.Valid f) (hF : F.card ≤ 2) (hne : 0 < F.card + D.length) (hW : S'.W + 14 * F.card ≤ S.W + 14 * (S.pairsMeeting F).card) : Step f S S'

A reduction restricting at most two parameters, and at least one parameter or constraint, with W' + 14 |F| ≤ W + 14 k, is a step of gate elimination.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.step_of_delete {n : ℕ} {f : BooleanFunction n} {S S' : State n} {N : ℕ ⊕ ℕ} (h : Reduction f S S' ∅ [N] [N]) (hS : S.Valid f) (hN : {u ∈ S.params | N ∈ S.children u}.card ≤ 2) : Step f S S'

Deleting one constraint with at most two parameters as parents is a step of gate elimination: only those parents may gain weight, each at most one.

Restrictions

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.reduction_restrict {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x : ℕ} (hx : x ∈ S.params) {ℓ : SemiCircuit.Lit} (hℓ : ∀ (y : ℕ), ℓ.Reads y → y ∈ S.params ∧ y ≠ x ∧ S.children x ⊆ S.children y ∧ (S.Paired x → S.IsPartner x y)) : Reduction f S (S.restrict x ℓ (S.pairsAvoid x)) {x} [] []

Restricting a parameter x to a constant, or to a literal of a remaining parameter y with at least the children of x and, if x is paired, its partner, is a reduction.

Fixing a parameter to a constant

def Cslib.Circuits.Boolean.AffineDisperser.State.fixConst {n : ℕ} (S : State n) (w : ℕ) (b : Bool) : State n

Fix the parameter w to the constant b, dropping the pair containing w, if any: the restriction (UF) for an unpaired parameter and (PF) for a paired one.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.restrictOK_fixConst {n : ℕ} {S : State n} {w : ℕ} (hw : w ∈ S.params) (b : Bool) : S.RestrictOK w (SemiCircuit.Lit.const b) (S.pairsAvoid w)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.fixConst {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {w : ℕ} (hw : w ∈ S.params) (b : Bool) : (S.fixConst w b).Valid f

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.fixConst_params {n : ℕ} (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).params = S.params.erase w

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.fixConst_pairs {n : ℕ} (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).pairs = S.pairsAvoid w

theorem Cslib.Circuits.Boolean.AffineDisperser.State.fixConst_size {n : ℕ} (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).size = S.size

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.State.fixConst_gate {n : ℕ} (S : State n) (w : ℕ) (b : Bool) (J : ℕ) : (S.fixConst w b).gate J = (S.gate J).subst w (SemiCircuit.Lit.const b)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.fixConst_children {n : ℕ} (S : State n) {w : ℕ} (b : Bool) {z : ℕ} (hz : z ≠ w) : (S.fixConst w b).children z = S.children z

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.reduction_fixConst {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {w : ℕ} (hw : w ∈ S.params) (b : Bool) : Reduction f S (S.fixConst w b) {w} [] []

Fixing a parameter to a constant is a reduction.

Deletions

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.reduction_deleteGate {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteGateOK J ℓ) {T : List (ℕ ⊕ ℕ)} (hT : ∀ (t : ℕ), ℓ.Reads t → Sum.inl J ∈ T) : Reduction f S (S.deleteGate J ℓ) ∅ [Sum.inl J] T

Deleting a gate is a reduction; it may reroute only to the parameter read by the literal.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.reduction_deleteConst {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} {c : Bool} (hJ : J ∈ S.gates) (hc : ∀ (val : ℕ → Bool), S.EqnsHold val → (S.gate J).eval val = c) : Reduction f S (S.deleteGate J (SemiCircuit.Lit.const c)) ∅ [Sum.inl J] []

Deleting a gate that is constant on the solutions of the affine system is a reduction rerouting nothing.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.reduction_deleteEqn {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : SemiCircuit.Lit} (h : S.DeleteEqnOK e v ℓ) {T : List (ℕ ⊕ ℕ)} (hT : ∀ (t : ℕ), ℓ.Reads t → Sum.inr e ∈ T) : Reduction f S (S.deleteEqn e v ℓ) ∅ [Sum.inr e] T

Deleting an equation v = ℓ is a reduction; it may reroute only to the parameter read by the literal.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.reduction_dropTrivialEqn {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e : ℕ} (he : e ∈ S.eqns) (hterms : (S.eqn e).terms = ∅) : Reduction f S (S.dropTrivialEqn e) ∅ [Sum.inr e] []

Deleting an equation without terms is a reduction rerouting nothing.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.terms_eq_empty_of_subset {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {e : ℕ} (he : e ∈ S.eqns) (hsub : (S.eqn e).terms ⊆ S.params) : (S.eqn e).terms = ∅

In a valid state, an equation whose terms are all parameters has no terms.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_delete {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {N : ℕ ⊕ ℕ} (hN : S.Deletable N) : ∃ (S' : State n), Reduction f S S' ∅ [N] [N]

A deletable constraint of a valid state is deleted by a reduction.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_deleteAll {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (l : List (ℕ ⊕ ℕ)) (hl : l.Nodup) (hdel : ∀ N ∈ l, S.Deletable N) : ∃ (S' : State n), Reduction f S S' ∅ l l

Distinct deletable constraints of a valid state are deleted by a reduction.