Khrapchenko's bound

For sets A of inputs where a formula is 1 and B of inputs where it is 0, let edges A B be the pairs in A × B at Hamming distance one. Khrapchenko's theorem says that every De Morgan formula separating A from B has at least |edges A B|² / (|A| · |B|) leaves (Formula.sq_card_edges_le, stated without division). A literal leaf can only separate along its own coordinate, so its edges form a partial matching, and a gate splits one side of the rectangle, where the Cauchy–Schwarz inequality makes the measure subadditive.

If every input of a nonempty A has at least s₁ neighbours in a nonempty B and every input of B has at least s₀ neighbours in A, every formula separating them has at least s₀ · s₁ leaves (Formula.mul_le_leaves_of_neighbours); taking the one-inputs and zero-inputs of f gives the bound for sensitive functions (leaves_ge_of_sensitive). Parity is sensitive to every coordinate everywhere, so every De Morgan formula for parity on n ≥ 1 bits has at least n² leaves (parity_sq_le_leaves). The inputs of weight k and k - 1 show that the threshold function "at least k ones" needs k · (n + 1 - k) leaves for 1 ≤ k ≤ n (threshold_mul_le_leaves), so strict majority needs ((n + 1) / 2)² leaves for odd n (majority_mul_le_leaves).

These corollaries use only the rectangle bound |edges A B|² ≤ M · |A| · |B| for sets A of one-inputs and B of zero-inputs of f (KhrapchenkoBound f M). They are proved for every such M (KhrapchenkoBound.mul_le_of_sensitive, KhrapchenkoBound.parity_sq_le, KhrapchenkoBound.threshold_mul_le, KhrapchenkoBound.majority_mul_le) and specialized to formulas, where M is the number of leaves (Formula.khrapchenkoBound), so other models that satisfy the rectangle bound inherit them.

Splitting the inputs in half gives formulas with exactly 4 ^ k leaves for parity on 2 ^ k bits, so formulaSize parity = n² when n is a power of two (formulaSize_parity_two_pow).

The Khrapchenko measure

def Algebraic.KW.diff {n : ℕ} (x y : Fin n → Bool) : Finset (Fin n)

The coordinates where two inputs differ.

Equations

• Algebraic.KW.diff x y = {i : Fin n | x i ≠ y i}

noncomputable def Algebraic.KW.edges {n : ℕ} (A B : Finset (Fin n → Bool)) : Finset ((Fin n → Bool) × (Fin n → Bool))

Pairs from A × B at Hamming distance one.

Equations

• Algebraic.KW.edges A B = {p ∈ A ×ˢ B | (Algebraic.KW.diff p.1 p.2).card = 1}

def Algebraic.KW.flip {n : ℕ} (x : Fin n → Bool) (i : Fin n) : Fin n → Bool

The input x with coordinate i flipped.

Equations

• Algebraic.KW.flip x i = Function.update x i !x i

theorem Algebraic.KW.diff_flip {n : ℕ} (x : Fin n → Bool) (i : Fin n) : diff x (flip x i) = {i}

theorem Algebraic.KW.eq_flip_of_diff {n : ℕ} {x y : Fin n → Bool} {i : Fin n} (hcard : (diff x y).card = 1) (hi : x i ≠ y i) : y = flip x i

An input at distance one from x whose difference contains i is x flipped at i.

def Algebraic.KW.Formula.Separates {n : ℕ} (F : Formula n) (A B : Finset (Fin n → Bool)) : Prop

A formula separates A from B when it is 1 on A and 0 on B.

Equations

• F.Separates A B = ((∀ x ∈ A, F.eval x = true) ∧ ∀ y ∈ B, F.eval y = false)

theorem Algebraic.KW.sq_add_le_of_sq_le {r₁ r₂ L₁ L₂ a b₁ b₂ : ℕ} (h₁ : r₁ ^ 2 ≤ L₁ * a * b₁) (h₂ : r₂ ^ 2 ≤ L₂ * a * b₂) : (r₁ + r₂) ^ 2 ≤ (L₁ + L₂) * a * (b₁ + b₂)

The arithmetic heart of Khrapchenko's bound: the measure r² / (a · b) is subadditive when one side of the rectangle is split.

theorem Algebraic.KW.card_edges_split_right {n : ℕ} (A B : Finset (Fin n → Bool)) (p : (Fin n → Bool) → Prop) [DecidablePred p] : (edges A B).card = (edges A (Finset.filter p B)).card + (edges A ({y ∈ B | ¬p y})).card

Splitting the zero side of a rectangle splits its edges.

theorem Algebraic.KW.card_edges_split_left {n : ℕ} (A B : Finset (Fin n → Bool)) (p : (Fin n → Bool) → Prop) [DecidablePred p] : (edges A B).card = (edges (Finset.filter p A) B).card + (edges ({x ∈ A | ¬p x}) B).card

Splitting the one side of a rectangle splits its edges.

theorem Algebraic.KW.card_edges_le_left_of_lit {n : ℕ} {i : Fin n} {b : Bool} {A B : Finset (Fin n → Bool)} (h : (Formula.lit i b).Separates A B) : (edges A B).card ≤ A.card

A literal separating A from B has at most |A| edges: each one-input has only one candidate partner, obtained by flipping the literal's coordinate.

theorem Algebraic.KW.card_edges_le_right_of_lit {n : ℕ} {i : Fin n} {b : Bool} {A B : Finset (Fin n → Bool)} (h : (Formula.lit i b).Separates A B) : (edges A B).card ≤ B.card

A literal separating A from B has at most |B| edges.

theorem Algebraic.KW.Formula.sq_card_edges_le {n : ℕ} (F : Formula n) (A B : Finset (Fin n → Bool)) : F.Separates A B → (edges A B).card ^ 2 ≤ F.leaves * A.card * B.card

Khrapchenko's theorem. If a De Morgan formula F is 1 on A and 0 on B, then |edges A B|² ≤ leaves F · |A| · |B|.

theorem Algebraic.KW.Formula.sq_card_edges_le_of_computes {n : ℕ} {F : Formula n} {f : Cslib.BooleanFunction n} (hF : F.Computes f) : (edges {x : Fin n → Bool | f x = true} {y : Fin n → Bool | f y = false}).card ^ 2 ≤ F.leaves * {x : Cslib.BitString n | f x = true}.card * {y : Cslib.BitString n | f y = false}.card

Khrapchenko's theorem for a formula computing f, on the full rectangle of one-inputs and zero-inputs.

def Algebraic.KW.KhrapchenkoBound {n : ℕ} (f : Cslib.BooleanFunction n) (M : ℕ) : Prop

M bounds the Khrapchenko measure of f: for every set A of one-inputs and every set B of zero-inputs of f, |edges A B|² ≤ M · |A| · |B|. A formula computing f gives this bound with M its number of leaves (Formula.khrapchenkoBound); the corollaries below depend only on this bound, not on the model of computation.

Equations

• Algebraic.KW.KhrapchenkoBound f M = ∀ (A B : Finset (Fin n → Bool)), (∀ x ∈ A, f x = true) → (∀ y ∈ B, f y = false) → (Algebraic.KW.edges A B).card ^ 2 ≤ M * A.card * B.card

theorem Algebraic.KW.Formula.khrapchenkoBound {n : ℕ} {F : Formula n} {f : Cslib.BooleanFunction n} (hF : F.Computes f) : KhrapchenkoBound f F.leaves

Khrapchenko's theorem as a bound on the measure of the computed function.

Neighbour counts

def Algebraic.KW.neighbours {n : ℕ} (S : Finset (Fin n → Bool)) (x : Fin n → Bool) : Finset (Fin n)

The coordinates at which flipping x lands in S.

Equations

• Algebraic.KW.neighbours S x = {i : Fin n | Algebraic.KW.flip x i ∈ S}

theorem Algebraic.KW.sum_card_neighbours_le_card_edges {n : ℕ} (A B : Finset (Fin n → Bool)) : ∑ x ∈ A, (neighbours B x).card ≤ (edges A B).card

Each input of A contributes its neighbours in B as edges.

theorem Algebraic.KW.diff_comm {n : ℕ} (x y : Fin n → Bool) : diff x y = diff y x

theorem Algebraic.KW.card_edges_comm {n : ℕ} (A B : Finset (Fin n → Bool)) : (edges B A).card = (edges A B).card

The edge count is symmetric in the two sides.

theorem Algebraic.KW.mul_le_of_neighbours {n : ℕ} {A B : Finset (Fin n → Bool)} {s₀ s₁ M : ℕ} (hE : (edges A B).card ^ 2 ≤ M * A.card * B.card) (hA : A.Nonempty) (hB : B.Nonempty) (h₁ : ∀ x ∈ A, s₁ ≤ (neighbours B x).card) (h₀ : ∀ y ∈ B, s₀ ≤ (neighbours A y).card) : s₀ * s₁ ≤ M

Neighbour counts against a measure bound. If |edges A B|² ≤ M · |A| · |B| for nonempty A and B, every input of A has at least s₁ neighbours in B, and every input of B has at least s₀ neighbours in A, then s₀ · s₁ ≤ M.

theorem Algebraic.KW.Formula.mul_le_leaves_of_neighbours {n : ℕ} {F : Formula n} {A B : Finset (Fin n → Bool)} {s₀ s₁ : ℕ} (hF : F.Separates A B) (hA : A.Nonempty) (hB : B.Nonempty) (h₁ : ∀ x ∈ A, s₁ ≤ (neighbours B x).card) (h₀ : ∀ y ∈ B, s₀ ≤ (neighbours A y).card) : s₀ * s₁ ≤ F.leaves

Khrapchenko's bound from neighbour counts. If a formula separates nonempty A from nonempty B, every input of A has at least s₁ neighbours in B, and every input of B has at least s₀ neighbours in A, the formula has at least s₀ · s₁ leaves.

Sensitive functions

def Algebraic.KW.sensitiveCoordinates {n : ℕ} (f : Cslib.BooleanFunction n) (x : Fin n → Bool) : Finset (Fin n)

The coordinates of x at which flipping changes f.

Equations

• Algebraic.KW.sensitiveCoordinates f x = {i : Fin n | f (Algebraic.KW.flip x i) ≠ f x}

theorem Algebraic.KW.KhrapchenkoBound.mul_le_of_sensitive {n : ℕ} {f : Cslib.BooleanFunction n} {s₀ s₁ M : ℕ} (hM : KhrapchenkoBound f M) (hone : ∃ (x : Cslib.BitString n), f x = true) (hzero : ∃ (y : Cslib.BitString n), f y = false) (h₁ : ∀ (x : Cslib.BitString n), f x = true → s₁ ≤ (sensitiveCoordinates f x).card) (h₀ : ∀ (y : Cslib.BitString n), f y = false → s₀ ≤ (sensitiveCoordinates f y).card) : s₀ * s₁ ≤ M

Sensitivity against a measure bound. If every one-input of f is sensitive on at least s₁ coordinates, every zero-input on at least s₀, and f takes both values, then every bound M on the Khrapchenko measure of f satisfies s₀ · s₁ ≤ M.

theorem Algebraic.KW.leaves_ge_of_sensitive {n : ℕ} {f : Cslib.BooleanFunction n} {s₀ s₁ : ℕ} (hone : ∃ (x : Cslib.BitString n), f x = true) (hzero : ∃ (y : Cslib.BitString n), f y = false) (h₁ : ∀ (x : Cslib.BitString n), f x = true → s₁ ≤ (sensitiveCoordinates f x).card) (h₀ : ∀ (y : Cslib.BitString n), f y = false → s₀ ≤ (sensitiveCoordinates f y).card) {F : Formula n} (hF : F.Computes f) : s₀ * s₁ ≤ F.leaves

Khrapchenko's bound for sensitive functions. If every one-input of f is sensitive on at least s₁ coordinates, every zero-input on at least s₀, and f takes both values, every De Morgan formula for f has at least s₀ · s₁ leaves.

Parity

theorem Algebraic.KW.parity_flip {n : ℕ} (x : Fin n → Bool) (i : Fin n) : GateElimination.Xor.parity (flip x i) = !GateElimination.Xor.parity x

theorem Algebraic.KW.sensitiveCoordinates_parity {n : ℕ} (x : Fin n → Bool) : sensitiveCoordinates GateElimination.Xor.parity x = Finset.univ

theorem Algebraic.KW.KhrapchenkoBound.parity_sq_le {n : ℕ} [NeZero n] {M : ℕ} (hM : KhrapchenkoBound GateElimination.Xor.parity M) : n ^ 2 ≤ M

Parity against a measure bound. Every bound on the Khrapchenko measure of the parity of n ≥ 1 bits is at least n².

theorem Algebraic.KW.parity_sq_le_leaves {n : ℕ} [NeZero n] {F : Formula n} (hF : F.Computes GateElimination.Xor.parity) : n ^ 2 ≤ F.leaves

Khrapchenko's bound for parity. Every De Morgan formula computing the parity of n ≥ 1 bits has at least n² leaves.

theorem Algebraic.KW.le_formulaSize_parity {n : ℕ} [NeZero n] : ↑(n ^ 2) ≤ formulaSize GateElimination.Xor.parity

Threshold functions

def Algebraic.KW.weight {n : ℕ} (x : Fin n → Bool) : ℕ

The number of ones in an input.

Equations

• Algebraic.KW.weight x = {i : Fin n | x i = true}.card

def Algebraic.KW.threshold {n : ℕ} (k : ℕ) : Cslib.BooleanFunction n

The threshold function: at least k of the inputs are one.

Equations

• Algebraic.KW.threshold k x = decide (k ≤ Algebraic.KW.weight x)

def Algebraic.KW.majority {n : ℕ} : Cslib.BooleanFunction n

Strict majority: more than half of the inputs are one (ties are false).

Equations

• Algebraic.KW.majority = Algebraic.KW.threshold (n / 2 + 1)

theorem Algebraic.KW.weight_flip_of_true {n : ℕ} {x : Fin n → Bool} {i : Fin n} (hi : x i = true) : weight (flip x i) + 1 = weight x

theorem Algebraic.KW.weight_flip_of_false {n : ℕ} {x : Fin n → Bool} {i : Fin n} (hi : x i = false) : weight (flip x i) = weight x + 1

def Algebraic.KW.prefixOnes {n : ℕ} (k : ℕ) : Fin n → Bool

An input whose first k coordinates are one and the rest zero.

Equations

• Algebraic.KW.prefixOnes k i = decide (↑i < k)

theorem Algebraic.KW.weight_prefixOnes {n k : ℕ} (hk : k ≤ n) : weight (prefixOnes k) = k

theorem Algebraic.KW.KhrapchenkoBound.threshold_mul_le {n k M : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) (hM : KhrapchenkoBound (threshold k) M) : (n + 1 - k) * k ≤ M

Threshold functions against a measure bound. For 1 ≤ k ≤ n, every bound on the Khrapchenko measure of "at least k of n inputs are one" is at least k · (n + 1 - k): the inputs of weight k and k - 1 form the rectangle.

theorem Algebraic.KW.threshold_mul_le_leaves {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) {F : Formula n} (hF : F.Computes (threshold k)) : (n + 1 - k) * k ≤ F.leaves

Khrapchenko's bound for threshold functions. For 1 ≤ k ≤ n, every De Morgan formula computing "at least k of n inputs are one" has at least k · (n + 1 - k) leaves: the inputs of weight k and k - 1 form the rectangle.

theorem Algebraic.KW.KhrapchenkoBound.majority_mul_le {n M : ℕ} (hn : 1 ≤ n) (hM : KhrapchenkoBound majority M) : (n - n / 2) * (n / 2 + 1) ≤ M

Majority against a measure bound. For n ≥ 1, every bound on the Khrapchenko measure of strict majority of n inputs is at least (n - ⌊n/2⌋) · (⌊n/2⌋ + 1).

theorem Algebraic.KW.majority_mul_le_leaves {n : ℕ} (hn : 1 ≤ n) {F : Formula n} (hF : F.Computes majority) : (n - n / 2) * (n / 2 + 1) ≤ F.leaves

Khrapchenko's bound for majority. Every De Morgan formula computing strict majority of n ≥ 1 inputs has at least (n - ⌊n/2⌋) · (⌊n/2⌋ + 1) leaves, which is ((n + 1)/2)² for odd n.

A matching upper bound at powers of two

theorem Algebraic.KW.parity_append {a b : ℕ} (x : Fin (a + b) → Bool) : GateElimination.Xor.parity x = (GateElimination.Xor.parity (x ∘ Fin.castAdd b) ^^ GateElimination.Xor.parity (x ∘ Fin.natAdd a))

def Algebraic.KW.Formula.xor {n : ℕ} (L R : Formula n) : Formula n

The formula (L ∧ ¬R) ∨ (¬L ∧ R) for the exclusive or of two formulas.

Equations

• L.xor R = (L.and R.neg).or (L.neg.and R)

@[simp]

theorem Algebraic.KW.Formula.eval_xor {n : ℕ} (L R : Formula n) (x : Fin n → Bool) : (L.xor R).eval x = (L.eval x ^^ R.eval x)

@[simp]

theorem Algebraic.KW.Formula.leaves_xor {n : ℕ} (L R : Formula n) : (L.xor R).leaves = 2 * (L.leaves + R.leaves)

def Algebraic.KW.parityFormula (k : ℕ) : Formula (2 ^ k)

Parity on 2 ^ k bits as a balanced formula with 4 ^ k leaves.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.KW.parityFormula 0 = Algebraic.KW.Formula.lit 0 true

theorem Algebraic.KW.parityFormula_computes (k : ℕ) : (parityFormula k).Computes GateElimination.Xor.parity

theorem Algebraic.KW.leaves_parityFormula (k : ℕ) : (parityFormula k).leaves = 4 ^ k

theorem Algebraic.KW.formulaSize_parity_two_pow (k : ℕ) : formulaSize GateElimination.Xor.parity = ↑((2 ^ k) ^ 2)

Formula size of parity. At n = 2 ^ k bits the minimum number of leaves of a De Morgan formula computing parity is exactly n².