Formula depth from Khrapchenko's bound

A De Morgan formula with at most d AND and OR gates on every path has at most 2 ^ d leaves (leafSize_le_two_pow_depthWith_binaryCost), so a function all of whose formulas have at least L leaves has formula depth at least ⌈log₂ L⌉, with negations free (clog_le_formulaDepth_of_le_leafSize). With Khrapchenko's bounds Jukna, Section 6.8, the parity of n bits has formula depth at least ⌈log₂ n ^ 2⌉ (clog_sq_le_formulaDepth_parity) [Khr71a], and the threshold function Th^n_k at least ⌈log₂ k (n + 1 - k)⌉ (clog_mul_le_formulaDepth_threshold) [Khr71b].

For parity this is tight up to one: Yablonskii's balanced formulas (Complexity/Computability/Circuit/Boolean/Yablonskii.lean) give the upper bound 2 ⌈log₂ n⌉. In particular the parity of 2 ^ k bits has formula depth exactly 2 k (formulaDepth_parity_two_pow), and for 0 < r ≤ 2 ^ k the parity of 2 ^ k + r bits has formula depth 2 k + 1 or 2 k + 2.

Main results

• Cslib.Circuits.Boolean.clog_le_formulaDepth_of_le_leafSize: a leaf-size lower bound L gives the formula depth lower bound ⌈log₂ L⌉.
• Cslib.Circuits.Boolean.clog_sq_le_formulaDepth_parity, Cslib.Circuits.Boolean.two_mul_log_le_formulaDepth_parity: the formula depth of the parity of n bits is at least ⌈log₂ n ^ 2⌉ ≥ 2 ⌊log₂ n⌋.
• Cslib.Circuits.Boolean.formulaDepth_parity_two_pow: the formula depth of the parity of 2 ^ k bits is 2 k.
• Cslib.Circuits.Boolean.two_mul_add_one_le_formulaDepth_parity, Cslib.Circuits.Boolean.formulaDepth_parity_two_pow_add_le: for 0 < r ≤ 2 ^ k, the formula depth of the parity of 2 ^ k + r bits is between 2 k + 1 and 2 k + 2.
• Cslib.Circuits.Boolean.clog_mul_le_formulaDepth_threshold, Cslib.Circuits.Boolean.clog_sq_div_four_le_formulaDepth_majority: formula depth lower bounds for threshold functions and majority.

References

• V. M. Khrapchenko, Method of determining lower bounds for the complexity of Π-schemes
• V. M. Khrapchenko, Complexity of the realization of a linear function in the class of Π-circuits
• S. V. Yablonskii, Realization of a linear function in the class of π-schemes
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.Circuits.Boolean.clog_le_formulaDepth_of_le_leafSize {n : ℕ} {f : BooleanFunction n} {L : ℕ} (h : ∀ (F : Formula signature n), F.Computes interpretation f → L ≤ F.leafSize) : Nat.clog 2 L ≤ formulaDepth f

If every De Morgan formula for f has at least L leaves, the formula depth of f, with negations free, is at least ⌈log₂ L⌉.

Parity

theorem Cslib.Circuits.Boolean.clog_sq_le_formulaDepth_parity (n : ℕ) : Nat.clog 2 (n ^ 2) ≤ formulaDepth (parity n)

The formula depth of the parity of n bits, with negations free, is at least ⌈log₂ n ^ 2⌉.

theorem Cslib.Circuits.Boolean.two_mul_log_le_formulaDepth_parity (n : ℕ) : 2 * Nat.log 2 n ≤ formulaDepth (parity n)

The formula depth of the parity of n bits, with negations free, is at least 2 log₂ n.

theorem Cslib.Circuits.Boolean.formulaDepth_parity_two_pow (k : ℕ) : formulaDepth (parity (2 ^ k)) = 2 * k

The formula depth of parity. The parity of 2 ^ k bits has formula depth 2 k, with negations free.

theorem Cslib.Circuits.Boolean.two_mul_add_one_le_formulaDepth_parity {k r : ℕ} (hr : 0 < r) : 2 * k + 1 ≤ formulaDepth (parity (2 ^ k + r))

For r > 0, the parity of 2 ^ k + r bits has formula depth at least 2 k + 1.

theorem Cslib.Circuits.Boolean.formulaDepth_parity_two_pow_add_le {k r : ℕ} (hr : r ≤ 2 ^ k) : formulaDepth (parity (2 ^ k + r)) ≤ 2 * k + 2

For r ≤ 2 ^ k, the parity of 2 ^ k + r bits has formula depth at most 2 k + 2.

Threshold functions

theorem Cslib.Circuits.Boolean.clog_mul_le_formulaDepth_threshold (n k : ℕ) : Nat.clog 2 (k * (n + 1 - k)) ≤ formulaDepth (threshold n k)

The threshold function Th^n_k has formula depth at least ⌈log₂ k (n + 1 - k)⌉, with negations free.

theorem Cslib.Circuits.Boolean.clog_sq_div_four_le_formulaDepth_majority (n : ℕ) : Nat.clog 2 ((n + 1) ^ 2 / 4) ≤ formulaDepth (majority n)

The majority of n bits has formula depth at least ⌈log₂ ⌊(n + 1) ^ 2 / 4⌋⌉, with negations free.