A 3.5 n - 7 d lower bound for affine dispersers

Theorem 4.1 of Mishra and Santhanam: every circuit over the full binary basis B₂ computing an affine disperser for dimension d on n bits has at least 3.5 n - 7 d gates (Cslib.Circuits.Boolean.AffineDisperser.seven_mul_le_two_mul_size_add). This improves the 3.1 n - o(n) lower bound of Li and Yang, itself improving the (3 + 1/86) n - o(n) bound of Find, Golovnev, Hirsch and Kulikov, whose fair semi-circuits (Cslib.Circuits.Boolean.SemiCircuit) carry the gate elimination.

The proof starts gate elimination from the circuit itself (initialState): its inputs are the parameters, its gates the acyclic part, the affine system is empty and the parameter map is the identity, so a = n and W ≤ 2 |C| + 7 n. Every valid state satisfies 14 a ≤ W + 14 d (State.Valid.fourteen_mul_a_le), by induction on m + s along the steps of Lemma 4.2 (State.Valid.exists_step), so 14 n ≤ 2 |C| + 7 n + 14 d.

The circuits are those of cslib over fullSignature 2 Bool, where a constant also costs a gate; the source lets circuits read constants for free, so the bound holds here a fortiori.

The development is organised as follows.

• AffineDisperser.State: the states of gate elimination, their potential, Proposition 2.2 and Lemma 2.3 of the source.
• AffineDisperser.Operations, AffineDisperser.Reparameterisation, AffineDisperser.Rewiring: the operations on states (restrictions and deletions; exchanging a parameter with an auxiliary variable and the quadratic substitution; moving and rewiring gates), with validity.
• AffineDisperser.Reduction: reductions, which restrict parameters and delete constraints, and their accounting, done once for all reductions.
• AffineDisperser.Deletion, AffineDisperser.Normal: the preliminary reductions of Section 4.1.
• AffineDisperser.MinimalAnd: restructuring the minimal AND, Section 4.2.
• AffineDisperser.Elimination: eliminating the minimal AND, Section 4.3.
• AffineDisperser.Step: Lemma 4.2, one step of gate elimination.

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.initialState: the initial state of gate elimination.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.fourteen_mul_a_le: the potential bound.
• Cslib.Circuits.Boolean.AffineDisperser.seven_mul_le_two_mul_size_add: Theorem 4.1.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits
• J. Li and T. Yang, 3.1n − o(n) Circuit Lower Bounds for Explicit Functions
• M. G. Find, A. Golovnev, E. A. Hirsch and A. S. Kulikov, A better-than-3n lower bound for the circuit complexity of an explicit function

The potential bound

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.fourteen_mul_a_le {n : ℕ} {f : BooleanFunction n} {d : ℕ} (hf : BitString.IsAffineDisperser f d) (S : State n) : S.Valid f → 14 * S.a ≤ S.W + 14 * d

Every valid state for an affine disperser for dimension d satisfies 14 a ≤ W + 14 d: apply Lemma 4.2 until a ≤ d, adding up ΔW ≤ 14 Δa.

The initial state of a circuit

def Cslib.Circuits.Boolean.AffineDisperser.initialState {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : State n

The initial state of gate elimination for a circuit: its semi-circuit (SemiCircuit.ofCircuit), whose parameters are the inputs, with no pairs and the parameter map reading the inputs.

theorem Cslib.Circuits.Boolean.AffineDisperser.initialState_valid {n : ℕ} {f : BooleanFunction n} {C : Circuit (fullSignature 2 Bool) n 1} (hC : C.Computes fullInterpretation (single f)) : (initialState C).Valid f

The initial state of a circuit computing f is valid.

theorem Cslib.Circuits.Boolean.AffineDisperser.initialState_a {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (initialState C).a = n

theorem Cslib.Circuits.Boolean.AffineDisperser.initialState_W_le {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) : (initialState C).W ≤ 2 * C.size + 7 * n

Theorem 4.1

theorem Cslib.Circuits.Boolean.AffineDisperser.seven_mul_le_two_mul_size_add {n : ℕ} {f : BooleanFunction n} {d : ℕ} (hf : BitString.IsAffineDisperser f d) (C : Circuit (fullSignature 2 Bool) n 1) (hC : C.Computes fullInterpretation (single f)) : 7 * n ≤ 2 * C.size + 14 * d

Theorem 4.1 of Mishra and Santhanam: every circuit over the full binary basis computing an affine disperser for dimension d on n bits has at least 3.5 n - 7 d gates, stated without subtraction as 7 n ≤ 2 |C| + 14 d.