Preliminary reductions of gate elimination

The six preliminary reductions of Mishra and Santhanam, Section 4.1, each a step of gate elimination (State.Step) from a state whose configuration it names. Every reduction but the deletion (D4) of State.Valid.unit_delete is a State.Reduction, so its accounting is that of State.Reduction.step or State.Reduction.step_of_delete.

• Case 1, State.DeletionAvailable: one of the deletions (D1)–(D4) applies (State.Valid.step_of_deletion, in AffineDisperser.Deletion).
• Case 2, State.AndOnIsolated: an AND-type gate reads an unpaired isolated parameter z and another parameter w; fixing w makes the gate constant and z unused (State.Valid.step_of_andOnIsolated).
• Case 3, State.DegeneratePair: a paired parameter has degree 0 or at least 2 (State.Valid.step_of_degeneratePair).
• Case 4, State.PartnersShareChild: two partners have a common child; restricting one to a literal of the other makes it constant (State.Valid.step_of_partnersShareChild).
• Case 5, State.PairInSystem: a paired parameter occurs in the affine system; fixing its partner leaves it to (D4) (State.Valid.step_of_pairInSystem).
• Case 6, State.AndOnPair: an AND-type gate reads a paired parameter and another parameter (State.Valid.step_of_andOnPair).

Before them, affine gates reading no gates are moved into the affine system (State.Valid.preparation_moveAffine). When no affine gate can be moved and neither Case 1 nor Case 2 applies, the state is exclusive (State.Valid.exclusive): no constraint has an unpaired isolated parameter and another parameter as parents. When none of the six cases applies, the state is normal (State.Normal, State.Valid.step_or_normal): it is exclusive, every parameter of the affine system is unpaired of degree at least two, and so is every parameter read by an AND-type gate.

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.AndOnIsolated, State.DegeneratePair, State.PartnersShareChild, State.PairInSystem, State.AndOnPair: the configurations of Cases 2 to 6.
• Cslib.Circuits.Boolean.AffineDisperser.State.Normal: normal states.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_andOnIsolated, step_of_degeneratePair, step_of_partnersShareChild, step_of_pairInSystem, step_of_andOnPair: the preliminary reductions are steps of gate elimination.
• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_or_normal: a state where no affine gate can be moved has a step or is normal.

References

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

Case 2: an AND-type gate on an isolated parameter

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

The configuration of Case 2: an AND-type gate reads an unpaired isolated parameter z and another parameter w.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_andOnIsolated {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (h : S.AndOnIsolated) : ∃ (S' : State n), Step f S S'

Case 2 of the preliminary reductions: fix w so that the AND-type gate becomes constant and delete it; z becomes unused. If w is unpaired, Δa = -1 and ΔW ≤ -14; otherwise the partner of w becomes unpaired, Δa = 0 and ΔW ≤ -4.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.two_le_deg_of_not_andOnIsolated {n : ℕ} {S : State n} (h2 : ¬S.AndOnIsolated) {G x y : ℕ} (hG : G ∈ S.gates) (hand : ¬SemiCircuit.IsAffineOp (S.gate G).op) (hargs : (S.gate G).left = SemiCircuit.Arg.node x ∧ (S.gate G).right = SemiCircuit.Arg.node y ∨ (S.gate G).left = SemiCircuit.Arg.node y ∧ (S.gate G).right = SemiCircuit.Arg.node x) (hxu : x ∈ S.unpaired) (hy : y ∈ S.params) (hxy : x ≠ y) : 2 ≤ S.deg x

When Case 2 does not apply, an unpaired parameter read by an AND-type gate together with another parameter has degree at least two.

Moving affine gates

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

An affine gate reading no gates, which is moved into the affine system before the preliminary reductions.

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

A name larger than every equation name.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.freshEqn_notMem {n : ℕ} (S : State n) : S.freshEqn ∉ S.eqns

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.preparation_moveAffine {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {J : ℕ} (hJ : S.Movable J) : Preparation f S (S.moveAffine J S.freshEqn)

Moving a movable gate into the affine system is a preparatory operation.

Exclusive states

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exclusive {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hmov : ∀ (J : ℕ), ¬S.Movable J) (hdel : ¬S.DeletionAvailable) (h2 : ¬S.AndOnIsolated) : S.Exclusive

Consequence of Cases 1 and 2 of Mishra and Santhanam: when no affine gate can be moved, no deletion applies and Case 2 does not apply, the unique child of an unpaired isolated parameter is a gate whose other input is not a parameter.

Case 3: a paired parameter of degree other than one

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

The configuration of Case 3: a paired parameter has degree 0 or at least 2.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deg_eq_one_of_not_degeneratePair {n : ℕ} {S : State n} (h3 : ¬S.DegeneratePair) {p : ℕ} (hp : p ∈ S.params) (hpp : S.Paired p) : S.deg p = 1

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_degeneratePair {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hexcl : S.Exclusive) (h : S.DegeneratePair) : ∃ (S' : State n), Step f S S'

Case 3 of the preliminary reductions. If a paired parameter p is unused, fixing its partner removes the pair: Δa = 0, ΔW ≤ -3. If p has two children, fixing p makes both deletable; the partner becomes unpaired and no other weight grows: Δa = 0, ΔW ≤ 0.

Case 4: partners with a common child

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletionAvailable_of_unary {n : ℕ} {S : State n} {J : ℕ} (hJ : J ∈ S.gates) (h : SemiCircuit.IsUnaryOp (S.gate J).op) : S.DeletionAvailable

A gate whose operation is a projection or a negated projection computes a literal of an input, so (D1) applies.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.deletionAvailable_of_const_op {n : ℕ} {S : State n} {J : ℕ} (hJ : J ∈ S.gates) (h : ∀ (a b : Bool), (S.gate J).op a b = (S.gate J).op false false) : S.DeletionAvailable

A gate with a constant operation computes a constant, so (D1) applies.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.eq_insert_of_mem_terms {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hdel : ¬S.DeletionAvailable) {e p r : ℕ} (he : e ∈ S.eqns) (hp : p ∈ S.params) (hr : r ∈ S.params) (hpr : p ≠ r) (hpe : p ∈ (S.eqn e).terms) (hre : r ∈ (S.eqn e).terms) : ∃ v ∈ S.aux, v ≠ p ∧ v ≠ r ∧ (S.eqn e).terms = {v, p, r}

When no deletion applies, an equation containing two parameters p and r reads v + p + r = rhs for an auxiliary variable v.

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

The configuration of Case 4: two partners have a common child.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.notMem_children_of_isPartner {n : ℕ} {S : State n} (h4 : ¬S.PartnersShareChild) {p r : ℕ} (hpr : S.IsPartner p r) {N : ℕ ⊕ ℕ} (hNp : N ∈ S.children p) : N ∉ S.children r

When Case 4 does not apply, partners have no common child.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_partnersShareChild {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hdel : ¬S.DeletionAvailable) (h3 : ¬S.DegeneratePair) (h : S.PartnersShareChild) : ∃ (S' : State n), Step f S S'

Case 4 of the preliminary reductions: if partners p and r have a common child H, impose p = r + c so that H becomes constant and delete it; r becomes unused: Δa = 0, ΔW ≤ -5.

Case 5: a paired parameter in the affine system

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

The configuration of Case 5: a paired parameter occurs in the affine system.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_pairInSystem {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (hexcl : S.Exclusive) (h3 : ¬S.DegeneratePair) (h4 : ¬S.PartnersShareChild) (h : S.PairInSystem) : ∃ (S' : State n), Step f S S'

Case 5 of the preliminary reductions: if a paired parameter p occurs in the affine system, fix its partner r and delete the unique child of r; then p is unpaired with at most one child, an equation, and (D4) removes it if it remains: Δa = 0, ΔW ≤ 0.

Case 6: an AND-type gate on a paired parameter

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

The configuration of Case 6: an AND-type gate reads a paired parameter p and another parameter w.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_andOnPair {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hexcl : S.Exclusive) (h2 : ¬S.AndOnIsolated) (h3 : ¬S.DegeneratePair) (h4 : ¬S.PartnersShareChild) (h5 : ¬S.PairInSystem) (h : S.AndOnPair) : ∃ (S' : State n), Step f S S'

Case 6 of the preliminary reductions: an AND-type gate G reads a paired parameter p with partner r and another parameter w. Fix r, fix w so that G becomes constant, and delete G and the unique child of r; p becomes unpaired and unused. If w is unpaired, Δa = -1 and ΔW ≤ -14; otherwise the partner of w becomes unpaired, Δa = 0 and ΔW ≤ -3.

Normal states

structure Cslib.Circuits.Boolean.AffineDisperser.State.Normal {n : ℕ} (S : State n) : Prop

A state in which no affine gate can be moved and no preliminary reduction applies, recorded by the consequences used to restructure and eliminate the minimal AND.

• not_movable (J : ℕ) : ¬S.Movable J

  No affine gate reading no gates remains.

• no_deletion : ¬S.DeletionAvailable

  No deletion applies.

• exclusive : S.Exclusive

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

• system_param (x : ℕ) : x ∈ S.params → ∀ e ∈ S.eqns, x ∈ (S.eqn e).terms → x ∈ S.unpaired ∧ 2 ≤ S.deg x

  Every parameter occurring in the affine system is unpaired of degree at least two.

• and_param (G : ℕ) : G ∈ S.gates → ¬SemiCircuit.IsAffineOp (S.gate G).op → ∀ (x y : ℕ), (S.gate G).left = SemiCircuit.Arg.node x ∧ (S.gate G).right = SemiCircuit.Arg.node y ∨ (S.gate G).left = SemiCircuit.Arg.node y ∧ (S.gate G).right = SemiCircuit.Arg.node x → x ∈ S.params → y ∈ S.params → x ≠ y → x ∈ S.unpaired ∧ 2 ≤ S.deg x

  Both parameters read by an AND-type gate are unpaired of degree at least two.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_or_normal {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (hmov : ∀ (J : ℕ), ¬S.Movable J) : (∃ (S' : State n), Step f S S') ∨ S.Normal

The preliminary reductions of Mishra and Santhanam, Section 4.1: if d < a and no affine gate can be moved, one of Cases 1 to 6 applies, giving a step of gate elimination, or the state is normal.