Lemma 4.2: one step of gate elimination

Lemma 4.2 of Mishra and Santhanam: if d < a, a valid state for an affine disperser for dimension d has a step of gate elimination (State.Valid.exists_step): a valid state with smaller m + s, Δa ∈ {0, -1, -2} and ΔW ≤ 14 Δa.

The proof follows Section 4 of the source. Movable affine gates are moved into the affine system first (State.Valid.preparation_moveAffine); then one of the preliminary reductions is a step, or the state is normal (State.Valid.step_or_normal). In a normal state the minimal gate is an AND-type gate on two distinct inputs among the parameters and auxiliary variables (State.Valid.exists_minGate). An auxiliary input is exchanged with a parameter (State.Valid.exists_preparation_auxIn_lt), a child of the minimal AND reading one of its inputs is rerouted (State.Valid.exists_preparation_childIn_lt), and the analysis restarts; once neither applies, eliminating the minimal AND is a step (State.Valid.step_of_minimalAnd). The preparatory operations keep m, s and a and do not increase W, and they terminate since each lowers, in lexicographic order, the number of gates, the number of auxiliary inputs of the minimal gate (State.auxIn) and the number of its children reading one of its parameter inputs (State.childIn). The proof establishes the existence of a step; unlike the source, it is not an algorithm, and no running time is claimed.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_step: Lemma 4.2.

References

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

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_step_aux {n : ℕ} {f : BooleanFunction n} {d : ℕ} (hf : BitString.IsAffineDisperser f d) (k₁ k₂ k₃ : ℕ) (S : State n) : S.gates.card = k₁ → S.auxIn = k₂ → S.childIn = k₃ → S.Valid f → d < S.a → ∃ (S' : State n), Step f S S'

Lemma 4.2, by induction on the number of gates, the number of auxiliary inputs of the minimal gate and the number of its children reading one of its parameter inputs.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_step {n : ℕ} {f : BooleanFunction n} {d : ℕ} {S : State n} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) : ∃ (S' : State n), Step f S S'

Lemma 4.2 of Mishra and Santhanam: if d < a, a valid state for an affine disperser for dimension d has a step of gate elimination: a valid state with smaller m + s, Δa ∈ {0, -1, -2} and ΔW ≤ 14 Δa.