Nechiporuk's bound

Nechiporuk's lemma: a formula over any basis of fan-in at most two (such as the full binary basis B₂, or the De Morgan basis) with l ≥ 1 leaves labelled by bits of a set Y has at most 16 ^ l / 4 subfunctions on Y (four_mul_card_subfunctions_le), and at most 2 if l = 0, so always at most 2 · 16 ^ l (card_subfunctions_le). Fixing the other bits turns every subformula without leaves in Y into a constant, every gate with one such argument into a unary function of the other, and leaves the l - 1 binary gates with two arguments that read Y; each of these computes one of the 16 binary Boolean functions.

Over disjoint blocks Y₁, …, Y_k this gives Nechiporuk's bound [Nec66], Jukna, Section 6.5: a formula of leaf size L over a basis of fan-in at most two computing f has ∏ᵢ |subfunctions f Yᵢ| ≤ 2 ^ (4 L + k) (prod_card_subfunctions_le), that is ∑ᵢ ⌈log₂ |subfunctions f Yᵢ|⌉ ≤ 4 L + k (sum_clog_card_subfunctions_le). Unlike Khrapchenko's bound, it holds for the full binary basis.

Main results

• Cslib.Circuits.Boolean.card_subfunctions_le: Nechiporuk's lemma.
• Cslib.Circuits.Boolean.prod_card_subfunctions_le, Cslib.Circuits.Boolean.sum_clog_card_subfunctions_le: Nechiporuk's bound.

References

• E. I. Nechiporuk, On a Boolean function
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

Closing under unary functions

Nechiporuk's lemma

theorem Cslib.Circuits.Boolean.isConst_of_mem_subfunctions {n : ℕ} {g : BooleanFunction n} {σ : Signature} {I : Interpretation σ Bool} {F : Formula σ n} {Y : Finset (Fin n)} (hF : Formula.leafSizeIn Y F = 0) (hg : g ∈ BitString.subfunctions (F.eval I) Y) : Function.IsConst g

The subfunctions of a formula with no leaf in Y are constant.

theorem Cslib.Circuits.Boolean.four_mul_card_subfunctions_le {n : ℕ} {σ : Signature} (harity : ∀ (op : σ.Op), σ.Arity op ≤ 2) (I : Interpretation σ Bool) (F : Formula σ n) {Y : Finset (Fin n)} (hl : Formula.leafSizeIn Y F ≠ 0) : 4 * (BitString.subfunctions (F.eval I) Y).card ≤ 16 ^ Formula.leafSizeIn Y F

Nechiporuk's lemma, refined constant: a formula over a basis of fan-in at most two with l ≥ 1 leaves labelled by bits of Y has at most 16 ^ l / 4 subfunctions on Y.

theorem Cslib.Circuits.Boolean.card_subfunctions_le {n : ℕ} {σ : Signature} (harity : ∀ (op : σ.Op), σ.Arity op ≤ 2) (I : Interpretation σ Bool) (F : Formula σ n) (Y : Finset (Fin n)) : (BitString.subfunctions (F.eval I) Y).card ≤ 2 * 16 ^ Formula.leafSizeIn Y F

Nechiporuk's lemma. A formula over a basis of fan-in at most two with l leaves labelled by bits of Y has at most 2 · 16 ^ l subfunctions on Y.

theorem Cslib.Circuits.Boolean.prod_card_subfunctions_le {n : ℕ} {σ : Signature} {I : Interpretation σ Bool} (harity : ∀ (op : σ.Op), σ.Arity op ≤ 2) {f : BooleanFunction n} {F : Formula σ n} (hF : F.Computes I f) {ι : Type u_1} {s : Finset ι} {Y : ι → Finset (Fin n)} (hY : (↑s).PairwiseDisjoint Y) : ∏ i ∈ s, (BitString.subfunctions f (Y i)).card ≤ 2 ^ (4 * F.leafSize + s.card)

Nechiporuk's bound. If a formula of leaf size L over a basis of fan-in at most two computes f, then for disjoint blocks Y i of bits, i ∈ s, the numbers of subfunctions of f on the blocks have product at most 2 ^ (4 L + |s|).

theorem Cslib.Circuits.Boolean.sum_clog_card_subfunctions_le {n : ℕ} {σ : Signature} {I : Interpretation σ Bool} (harity : ∀ (op : σ.Op), σ.Arity op ≤ 2) {f : BooleanFunction n} {F : Formula σ n} (hF : F.Computes I f) {ι : Type u_1} {s : Finset ι} {Y : ι → Finset (Fin n)} (hY : (↑s).PairwiseDisjoint Y) : ∑ i ∈ s, Nat.clog 2 (BitString.subfunctions f (Y i)).card ≤ 4 * F.leafSize + s.card

Nechiporuk's bound, logarithmic form: the binary logarithms, rounded up, of the numbers of subfunctions on disjoint blocks add up to at most 4 L + |s|.