Eliminating the minimal AND

Section 4.3 of Mishra and Santhanam: in a normal state with d < a, eliminating a minimal AND G on the inputs x and y (State.MinimalAnd) is a step of gate elimination (State.Valid.step_of_minimalAnd):

• Case 7, State.SharedSecondChild: deg x = deg y = 2 and x, y share their second child B; restricting to a line of 𝔽₂² on which G and B are constant (exists_line_const) deletes both (State.Valid.step_of_sharedSecondChild), ΔW ≤ -18, Δa = -1;
• the bottleneck configuration, State.Bottleneck: deg x = 2 and the unique child D of G reads an unpaired isolated parameter z. If D is AND-type, fixing x and y makes G and D constant (Case 9, State.Valid.step_of_bottleneck_and, ΔW ≤ -28, Δa = -2); otherwise D is XOR-type and the quadratic reparameterisation deletes G and D (Case 10, State.Valid.step_of_bottleneck_xor, ΔW ≤ -14, Δa = -1);
• Case 8, otherwise: fixing x so that G becomes constant deletes all children of x and of G (State.Valid.step_fixInput), Δa = -1; only the unpaired isolated parameters below G can gain weight, at most deg G of them (State.Valid.card_isolated_le, State.Reduction.wt_add_le_fixInput).

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State.SharedSecondChild, Cslib.Circuits.Boolean.AffineDisperser.State.Bottleneck: the configurations of Section 4.3.
• Cslib.Circuits.Boolean.AffineDisperser.State.IsolatedBelow, Cslib.Circuits.Boolean.AffineDisperser.State.fixInputDeleted: unpaired isolated parameters sharing a child with G and constraints deleted by fixing an input of G.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_minimalAnd: eliminating the minimal AND 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

Case 7: a shared second child

def Cslib.Circuits.Boolean.AffineDisperser.State.SharedSecondChild {n : ℕ} (S : State n) (G x y : ℕ) : Prop

The configuration of Case 7 of Mishra and Santhanam: deg x = 2 and the inputs of the minimal AND share their second child B.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_sharedSecondChild {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hN : S.Normal) {G x y : ℕ} (h : S.MinimalAnd G x y) (h7 : S.SharedSecondChild G x y) : ∃ (S' : State n), Step f S S'

Case 7 of Mishra and Santhanam, Section 4.3: if both inputs x, y of the minimal AND have degree two and share their second child B, restrict to a line of 𝔽₂² on which both G and B are constant (exists_line_const) and delete both; the other input becomes unused: Δa = -1, ΔW ≤ -18.

Case 8: fixing an input

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

The bottleneck configuration of Mishra and Santhanam, Section 4.3: deg x = 2 and the minimal AND G has a unique child D, which reads an unpaired isolated parameter z.

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

The unpaired isolated parameters whose only child is a child of the gate G: they may gain weight when G becomes constant.

@[instance_reducible]

instance Cslib.Circuits.Boolean.AffineDisperser.State.instDecidablePredNatIsolatedBelow {n : ℕ} (S : State n) (G : ℕ) : DecidablePred (S.IsolatedBelow G)

Decidability of State.IsolatedBelow.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.card_isolated_le {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {G : ℕ} (hG : G ∈ S.gates) (s : Finset ℕ) (hs : s ⊆ S.params) : (Finset.filter (S.IsolatedBelow G) s).card ≤ S.deg G

At most deg G unpaired isolated parameters have their child among the children of the gate G: a child of G has at most one parent other than G.

def Cslib.Circuits.Boolean.AffineDisperser.State.fixInputDeleted {n : ℕ} (S : State n) (G x : ℕ) : Finset (ℕ ⊕ ℕ)

The constraints deleted by fixing the input x of the minimal AND G, besides G itself: the other children of x and the children of G.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Reduction.wt_add_le_fixInput {n : ℕ} {f : BooleanFunction n} {S S' : State n} (hS : S.Valid f) (hN : S.Normal) {G x y : ℕ} (h : S.MinimalAnd G x y) (h7 : ¬S.SharedSecondChild G x y) (hred : Reduction f S S' {x} (Sum.inl G :: (S.fixInputDeleted G x).toList) (S.fixInputDeleted G x).toList) {u : ℕ} (hux : u ≠ x) : (S'.wt u + if u = y ∧ S.deg x = 2 then 1 else 0) ≤ S.wt u + if S.IsolatedBelow G u then 1 else 0

The weights after fixing an input of the minimal AND: outside Case 7, only an unpaired isolated parameter below G gains weight, at most one, and y loses one when deg x = 2.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_fixInput {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hN : S.Normal) {G x y : ℕ} (h : S.MinimalAnd G x y) (h7 : ¬S.SharedSecondChild G x y) (hbot : ¬S.Bottleneck G x) : ∃ (S' : State n), Step f S S'

Case 8 of Mishra and Santhanam, Section 4.3: outside Case 7 and the bottleneck configuration, fix the input x of the minimal AND G so that G becomes constant and delete all children of x and of G. Only the k₁ ≤ k = deg G unpaired isolated parameters below G may gain weight, and y drops to weight six when deg x = 2: Δa = -1, ΔW ≤ -7 - 2 (deg x + k) + k₁ - [deg x = 2] ≤ -14.

Cases 9 and 10: the bottleneck

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_bottleneck_and {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hN : S.Normal) {G x y D z : ℕ} (h : S.MinimalAnd G x y) (h7 : ¬S.SharedSecondChild G x y) (hx2 : S.deg x = 2) (hDiff : ∀ K ∈ S.gates, (S.gate K).Reads G ↔ K = D) (hD : D ∈ S.gates) (hz : z ∈ S.unpaired) (hz1 : S.deg z = 1) (hDz : (S.gate D).Reads z) (hDand : ¬SemiCircuit.IsAffineOp (S.gate D).op) : ∃ (S' : State n), Step f S S'

Case 9 of Mishra and Santhanam, Section 4.3: in the bottleneck configuration with D AND-type, fix x and y so that D becomes constant and delete G, D and the second children of x and y; z becomes unused: Δa = -2, ΔW ≤ -28.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_bottleneck_xor {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (hN : S.Normal) {G x y D z : ℕ} (h : S.MinimalAnd G x y) (hDiff : ∀ K ∈ S.gates, (S.gate K).Reads G ↔ K = D) (hD : D ∈ S.gates) (hz : z ∈ S.unpaired) (hz1 : S.deg z = 1) (hDz : (S.gate D).Reads z) (hDaff : SemiCircuit.IsAffineOp (S.gate D).op) : ∃ (S' : State n), Step f S S'

Case 10 of Mishra and Santhanam, Section 4.3: in the bottleneck configuration with D affine, D is XOR-type since no deletion applies, and the quadratic reparameterisation deletes G and D: Δa = -1, ΔW ≤ -14.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_of_minimalAnd {n : ℕ} {f : BooleanFunction n} {S : State n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (hN : S.Normal) {G x y : ℕ} (h : S.MinimalAnd G x y) : ∃ (S' : State n), Step f S S'

Section 4.3 of Mishra and Santhanam: in a normal state with d < a, eliminating the minimal AND is a step of gate elimination.