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.

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.Reduction.step_of_shared {n : ℕ} {f : BooleanFunction n} {S S' : State n} (hS : S.Valid f) {G x' y' : ℕ} {B : ℕ ⊕ ℕ} (hx' : x' ∈ S.unpaired) (hy' : y' ∈ S.unpaired) (hxy : x' ≠ y') (hx'2 : S.deg x' = 2) (hy'2 : S.deg y' = 2) (hcy : S.children y' = {Sum.inl G, B}) (h : Reduction f S S' {x'} [Sum.inl G, B] []) : Step f S S'

Restricting one input x' of the minimal AND and deleting its two children G and B, which are also the children of the other input y', is a step: Δa = -1, ΔW ≤ -18.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_restrict_deleteConst {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x' : ℕ} (hx' : x' ∈ S.params) {ℓ : SemiCircuit.Lit} (hℓ : ∀ (t : ℕ), ℓ.Reads t → t ∈ S.params ∧ t ≠ x' ∧ S.children x' ⊆ S.children t ∧ (S.Paired x' → S.IsPartner x' t)) {G B : ℕ} (hG : G ∈ S.gates) (hB : B ∈ S.gates) (hBG : B ≠ G) (hBGr : ¬(S.gate B).Reads G) {c₁ c₂ : Bool} (hGc : ∀ (val : ℕ → Bool), (S.gate G).eval (Function.update val x' (ℓ.eval val)) = c₁) (hBc : ∀ (val : ℕ → Bool), (S.gate B).eval (Function.update val x' (ℓ.eval val)) = c₂) : ∃ (S' : State n), Reduction f S S' {x'} [Sum.inl G, Sum.inl B] []

Restricting a parameter x' to a constant or to a literal of another parameter with at least its children, on which the gates G and B ≠ G, B not reading G, are constant, and deleting both gates, is a reduction.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_sharedGate {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {G x y B : ℕ} (h : S.MinimalAnd G x y) (hcx : S.children x = {Sum.inl G, Sum.inl B}) (hcy : S.children y = {Sum.inl G, Sum.inl B}) (hBG : B ≠ G) : ∃ (S' : State n) (x' : ℕ) (y' : ℕ), (x' = x ∧ y' = y ∨ x' = y ∧ y' = x) ∧ Reduction f S S' {x'} [Sum.inl G, Sum.inl B] []

Case 7 when the shared second child B of x and y is a gate: on one of the lines x = c, y = c or x = y + c both G and B are constant, and restricting to it deletes both.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_sharedEqn {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (hN : S.Normal) {G x y e : ℕ} (h : S.MinimalAnd G x y) (hcx : S.children x = {Sum.inl G, Sum.inr e}) (hcy : S.children y = {Sum.inl G, Sum.inr e}) : ∃ (S' : State n), Reduction f S S' {x} [Sum.inl G, Sum.inr e] []

Case 7 when the shared second child of x and y is an equation v + x + y = rhs: restricting to the line x = y + c on which G is constant makes the equation read v = rhs + c, and both are deleted.

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)

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.Valid.exists_reduction_fixInput {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {G x y : ℕ} (h : S.MinimalAnd G x y) : ∃ (S' : State n), Reduction f S S' {x} (Sum.inl G :: (S.fixInputDeleted G x).toList) (S.fixInputDeleted G x).toList

Fixing the input x of the minimal AND so that G becomes constant, and deleting G, the other children of x and the children of G, is a reduction deleting deg x + deg G constraints.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.length_fixInput {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {G x y : ℕ} (h : S.MinimalAnd G x y) : (Sum.inl G :: (S.fixInputDeleted G x).toList).length = S.deg x + S.deg 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.MinimalAnd.not_isolatedBelow {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {G x y : ℕ} (h : S.MinimalAnd G x y) (hbot : ¬S.Bottleneck G x) (hx2 : S.deg x = 2) (hG1 : S.deg G = 1) {u : ℕ} : ¬S.IsolatedBelow G u

Outside the bottleneck configuration, when deg x = 2 and G has one child, no unpaired isolated parameter lies below G.

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.QuadOK.wt_add_le {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool} (h : S.QuadOK x y z G D α β γ c) (hx : 2 ≤ S.deg x) (hy : 2 ≤ S.deg y) (u : ℕ) : u ∈ insert D S.params → (S.quad x y z G D α β γ c).wt u + (((if u = x then 7 else 0) + if u = y then 7 else 0) + if u = z then 6 else 0) ≤ S.wt u + if u = D then 7 else 0

The weights after the quadratic reparameterisation: x and y become paired, z is replaced by D, which gains at most seven, and no other weight grows.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.step_quad {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool} (h : S.QuadOK x y z G D α β γ c) (hx : 2 ≤ S.deg x) (hy : 2 ≤ S.deg y) : Step f S (S.quad x y z G D α β γ c)

The quadratic reparameterisation of the bottleneck configuration, when x and y have degree at least two, is a step of gate elimination: Δa = -1, ΔW ≤ -14.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd.children_of_bottleneck {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {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) (hz1 : S.deg z = 1) (hDz : (S.gate D).Reads z) : S.children G = {Sum.inl D} ∧ S.children z = {Sum.inl D}

In the bottleneck configuration, G has the unique child D and z the unique child D.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_reduction_bottleneck_and {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {G x y D : ℕ} (h : S.MinimalAnd G x y) (hD : D ∈ S.gates) (hDG' : D ≠ G) {δ c : Bool} (hc : ∀ (val : ℕ → Bool), val G = δ → (S.gate D).eval val = c) {x₀ y₀ : Bool} (hδ : (S.gate G).eval (Function.update (Function.update (fun (x : ℕ) => false) y y₀) x x₀) = δ) {Bx By : ℕ ⊕ ℕ} (hBx : Bx ∈ S.children x) (hBy : By ∈ S.children y) (hBxG : Bx ≠ Sum.inl G) (hByG : By ≠ Sum.inl G) (hBxy : Bx ≠ By) (hBxD : Bx ≠ Sum.inl D) (hByD : By ≠ Sum.inl D) : ∃ (S' : State n), Reduction f S S' {x, y} [Sum.inl G, Sum.inl D, Bx, By] [Bx, By]

In the bottleneck configuration with D AND-type, fixing x and y so that G takes the value making D constant deletes G, D and the second children Bx, By of x and y.

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_bottleneck {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) (h7 : ¬S.SharedSecondChild G x y) (hbot : S.Bottleneck G x) : ∃ (S' : State n), Step f S S'

Cases 9 and 10 of Mishra and Santhanam, Section 4.3, the bottleneck configuration: the unique child D of the minimal AND G reads an unpaired isolated parameter z; its elimination is a step.

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.