Nechiporuk's bound for element distinctness

Element distinctness reads m blocks of k bits and says whether the blocks are pairwise different (elementDistinctness). With blocks of 2 t bits and m ≤ 2 ^ t, it has at least 2 ^ (t (m - 1)) subfunctions on each block: give the other blocks the values (j, wⱼ), tagged by their position j, and each choice of the wⱼ is told apart by its own set of forbidden values for the remaining block. Nechiporuk's bound then shows that a formula for it of leaf size L over any basis of fan-in at most two, such as the full binary basis, has m (m - 1) t ≤ 4 L + m (mul_le_leafSize_of_computes_elementDistinctness) [Nec66], Jukna, Section 6.5. Taking t = ⌈log₂ m⌉ (mul_clog_le_leafSize_of_computes_elementDistinctness), the n = 2 m ⌈log₂ m⌉ bits need leaf size about m ^ 2 log₂ m / 4, which is of order n ^ 2 / log n.

Main definitions

• Cslib.Circuits.Boolean.elementDistinctness: whether m blocks of k bits are distinct.

Main results

• Cslib.Circuits.Boolean.mul_le_leafSize_of_computes_elementDistinctness: Nechiporuk's bound for element distinctness.

References

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

def Cslib.Circuits.Boolean.elementDistinctness (m k : ℕ) : BooleanFunction (m * k)

Element distinctness: whether the m blocks of k bits are pairwise different.

theorem Cslib.Circuits.Boolean.two_pow_le_card_subfunctions_elementDistinctness {m t : ℕ} (hm : m ≤ 2 ^ t) (i : Fin m) : 2 ^ (t * (m - 1)) ≤ (BitString.subfunctions (elementDistinctness m (t + t)) (BitString.blockBits (t + t) i)).card

Element distinctness has at least 2 ^ (t (m - 1)) subfunctions on each block of 2 t bits when m ≤ 2 ^ t.

theorem Cslib.Circuits.Boolean.mul_le_leafSize_of_computes_elementDistinctness {m t : ℕ} {σ : Signature} (harity : ∀ (op : σ.Op), σ.Arity op ≤ 2) {I : Interpretation σ Bool} (hm : m ≤ 2 ^ t) {F : Formula σ (m * (t + t))} (hF : F.Computes I (elementDistinctness m (t + t))) : m * (m - 1) * t ≤ 4 * F.leafSize + m

Nechiporuk's bound for element distinctness. For m ≤ 2 ^ t, a formula over a basis of fan-in at most two deciding whether m blocks of 2 t bits are pairwise different has leaf size L with m (m - 1) t ≤ 4 L + m.

theorem Cslib.Circuits.Boolean.mul_clog_le_leafSize_of_computes_elementDistinctness {m : ℕ} {σ : Signature} (harity : ∀ (op : σ.Op), σ.Arity op ≤ 2) {I : Interpretation σ Bool} {F : Formula σ (m * (Nat.clog 2 m + Nat.clog 2 m))} (hF : F.Computes I (elementDistinctness m (Nat.clog 2 m + Nat.clog 2 m))) : m * (m - 1) * Nat.clog 2 m ≤ 4 * F.leafSize + m

With blocks of 2 ⌈log₂ m⌉ bits, a formula over a basis of fan-in at most two for element distinctness of m blocks has leaf size L with m (m - 1) ⌈log₂ m⌉ ≤ 4 L + m.