Composition of Boolean functions and the KRW conjecture

The composition f ⋄ g of f on m bits with g on n bits applies f to the values of g on m disjoint blocks of n bits. Here depth and size are the minimum depth and leaf count of a De Morgan formula (formulaDepth, formulaSize). Substituting a formula for g into a formula for f gives, for all f and g, depth (f ⋄ g) ≤ depth f + depth g (formulaDepth_compose_le) and size (f ⋄ g) ≤ size f · size g (formulaSize_compose_le). Projections give depth g ≤ depth (f ⋄ g) when f is not constant and depth f ≤ depth (f ⋄ g) when g is not constant.

The Karchmer–Raz–Wigderson conjecture asserts that for non-constant f and g the upper bounds are tight up to lower-order terms. It is stated here in its strong form, with a constant slack. KRWDepthWith c says that depth f + depth g ≤ depth (f ⋄ g) + c for all m, n and all non-constant f and g (NonConstant), and KRWSizeWith c says that size f · size g ≤ c · size (f ⋄ g) for all such f and g. The conjectures KRWDepth and KRWSize say that some constant c works. They are open, and nothing here proves them; forms whose slack grows with m or n are not formalized.

Both non-constancy hypotheses are needed. If f or g is constant then f ⋄ g is constant, and dropping either hypothesis from KRWDepthWith c or KRWSizeWith c gives a false statement for every c (not_forall_depth_of_constant_inner, not_forall_depth_of_constant_outer, not_forall_size_of_constant_inner, not_forall_size_of_constant_outer).

Relabeling and substitution

def Algebraic.KW.Formula.mapIndex {n N : ℕ} (φ : Fin n → Fin N) : Formula n → Formula N

Relabel the variables of a formula.

Equations

• Algebraic.KW.Formula.mapIndex φ (Algebraic.KW.Formula.lit i b) = Algebraic.KW.Formula.lit (φ i) b
• Algebraic.KW.Formula.mapIndex φ (Algebraic.KW.Formula.const b) = Algebraic.KW.Formula.const b
• Algebraic.KW.Formula.mapIndex φ (l.and r) = (Algebraic.KW.Formula.mapIndex φ l).and (Algebraic.KW.Formula.mapIndex φ r)
• Algebraic.KW.Formula.mapIndex φ (l.or r) = (Algebraic.KW.Formula.mapIndex φ l).or (Algebraic.KW.Formula.mapIndex φ r)

@[simp]

theorem Algebraic.KW.Formula.eval_mapIndex {n N : ℕ} (φ : Fin n → Fin N) (F : Formula n) (x : Fin N → Bool) : (mapIndex φ F).eval x = F.eval (x ∘ φ)

@[simp]

theorem Algebraic.KW.Formula.depth_mapIndex {n N : ℕ} (φ : Fin n → Fin N) (F : Formula n) : (mapIndex φ F).depth = F.depth

@[simp]

theorem Algebraic.KW.Formula.leaves_mapIndex {n N : ℕ} (φ : Fin n → Fin N) (F : Formula n) : (mapIndex φ F).leaves = F.leaves

def Algebraic.KW.Formula.subst {n N : ℕ} (σ : Fin N → Formula n) : Formula N → Formula n

Substitute a formula, or its negation, for every literal.

Equations

• Algebraic.KW.Formula.subst σ (Algebraic.KW.Formula.lit i b) = if b = true then σ i else (σ i).neg
• Algebraic.KW.Formula.subst σ (Algebraic.KW.Formula.const b) = Algebraic.KW.Formula.const b
• Algebraic.KW.Formula.subst σ (l.and r) = (Algebraic.KW.Formula.subst σ l).and (Algebraic.KW.Formula.subst σ r)
• Algebraic.KW.Formula.subst σ (l.or r) = (Algebraic.KW.Formula.subst σ l).or (Algebraic.KW.Formula.subst σ r)

@[simp]

theorem Algebraic.KW.Formula.eval_subst {n N : ℕ} (σ : Fin N → Formula n) (F : Formula N) (x : Fin n → Bool) : (subst σ F).eval x = F.eval fun (i : Fin N) => (σ i).eval x

theorem Algebraic.KW.Formula.depth_subst_le {n N : ℕ} (σ : Fin N → Formula n) {d : ℕ} (hσ : ∀ (i : Fin N), (σ i).depth ≤ d) (F : Formula N) : (subst σ F).depth ≤ F.depth + d

theorem Algebraic.KW.Formula.leaves_subst_le {n N : ℕ} (σ : Fin N → Formula n) {L : ℕ} (hL : 1 ≤ L) (hσ : ∀ (i : Fin N), (σ i).leaves ≤ L) (F : Formula N) : (subst σ F).leaves ≤ F.leaves * L

theorem Algebraic.KW.Formula.exists_computes (n : ℕ) (f : Cslib.BooleanFunction n) : ∃ (F : Formula n), F.Computes f

Every Boolean function has a De Morgan formula, by Shannon expansion.

theorem Algebraic.KW.exists_iInf_natCast_eq {ι : Type u_1} [Nonempty ι] (u : ι → ℕ) : ∃ (i : ι), ⨅ (j : ι), ↑(u j) = ↑(u i)

An infimum of natural numbers in ℕ∞ over a nonempty index type is attained.

Composition

def Algebraic.KW.blockIndex {m n : ℕ} (j : Fin m) (i : Fin n) : Fin (m * n)

The position of coordinate i of block j.

Equations

• Algebraic.KW.blockIndex j i = finProdFinEquiv (j, i)

theorem Algebraic.KW.finProdFinEquiv_symm_blockIndex {m n : ℕ} (j : Fin m) (i : Fin n) : finProdFinEquiv.symm (blockIndex j i) = (j, i)

def Algebraic.KW.compose {m n : ℕ} (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n) : Cslib.BooleanFunction (m * n)

The composition f ⋄ g: f applied to g on m disjoint blocks of n bits.

Equations

• Algebraic.KW.compose f g z = f fun (j : Fin m) => g fun (i : Fin n) => z (Algebraic.KW.blockIndex j i)

def Algebraic.KW.Formula.compose {m n : ℕ} (F : Formula m) (G : Formula n) : Formula (m * n)

Substitute a formula for g into a formula for f, block by block.

Equations

• F.compose G = Algebraic.KW.Formula.subst (fun (j : Fin m) => Algebraic.KW.Formula.mapIndex (Algebraic.KW.blockIndex j) G) F

theorem Algebraic.KW.Formula.eval_compose {m n : ℕ} (F : Formula m) (G : Formula n) (z : Fin (m * n) → Bool) : (F.compose G).eval z = F.eval fun (j : Fin m) => G.eval fun (i : Fin n) => z (blockIndex j i)

theorem Algebraic.KW.Formula.compose_computes {m n : ℕ} {F : Formula m} {G : Formula n} {f : Cslib.BooleanFunction m} {g : Cslib.BooleanFunction n} (hF : F.Computes f) (hG : G.Computes g) : (F.compose G).Computes (KW.compose f g)

theorem Algebraic.KW.Formula.depth_compose_le {m n : ℕ} (F : Formula m) (G : Formula n) : (F.compose G).depth ≤ F.depth + G.depth

theorem Algebraic.KW.Formula.leaves_compose_le {m n : ℕ} (F : Formula m) (G : Formula n) : (F.compose G).leaves ≤ F.leaves * G.leaves

instance Algebraic.KW.instNonemptySubtypeFormulaComputes {n : ℕ} (f : Cslib.BooleanFunction n) : Nonempty { F : Formula n // F.Computes f }

theorem Algebraic.KW.formulaDepth_ne_top {n : ℕ} (f : Cslib.BooleanFunction n) : formulaDepth f ≠ ⊤

Every function has finite formula depth.

theorem Algebraic.KW.formulaDepth_compose_le {m n : ℕ} (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n) : formulaDepth (compose f g) ≤ formulaDepth f + formulaDepth g

Composition adds at most the depths.

theorem Algebraic.KW.formulaSize_compose_le {m n : ℕ} (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n) : formulaSize (compose f g) ≤ formulaSize f * formulaSize g

Composition multiplies at most the sizes.

Lower bounds by projection

theorem Algebraic.KW.exists_sensitive_of_ne {m : ℕ} {f : Cslib.BooleanFunction m} {a₀ a₁ : Fin m → Bool} (h : f a₀ ≠ f a₁) : ∃ (j : Fin m) (a : Fin m → Bool), f (Function.update a j true) ≠ f (Function.update a j false)

A non-constant function is sensitive at some point in some coordinate.

theorem Algebraic.KW.formulaDepth_inner_le_compose {m n : ℕ} {f : Cslib.BooleanFunction m} {g : Cslib.BooleanFunction n} {j : Fin m} {a : Fin m → Bool} (hf : f (Function.update a j true) ≠ f (Function.update a j false)) {x₀ x₁ : Fin n → Bool} (h₀ : g x₀ = false) (h₁ : g x₁ = true) : formulaDepth g ≤ formulaDepth (compose f g)

The depth of the inner function is at most the depth of the composition, when the outer function is sensitive at some point.

theorem Algebraic.KW.formulaDepth_outer_le_compose {m n : ℕ} {f : Cslib.BooleanFunction m} {g : Cslib.BooleanFunction n} {x₀ x₁ : Fin n → Bool} (h₀ : g x₀ = false) (h₁ : g x₁ = true) : formulaDepth f ≤ formulaDepth (compose f g)

The depth of the outer function is at most the depth of the composition, when the inner function is not constant.

Non-constant functions

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

A Boolean function is non-constant when it takes two different values.

Equations

• Algebraic.KW.NonConstant f = ∃ (x : Cslib.BitString n) (y : Cslib.BitString n), f x ≠ f y

theorem Algebraic.KW.NonConstant.exists_eq_false_eq_true {n : ℕ} {f : Cslib.BooleanFunction n} (h : NonConstant f) : ∃ (x₀ : Cslib.BitString n) (x₁ : Cslib.BitString n), f x₀ = false ∧ f x₁ = true

A non-constant function takes the value false somewhere and true somewhere.

theorem Algebraic.KW.forall_eq_of_not_nonConstant {n : ℕ} {f : Cslib.BooleanFunction n} (h : ¬NonConstant f) (x : Cslib.BitString n) : f x = f fun (x : Fin n) => false

A function that is not non-constant takes a single value.

theorem Algebraic.KW.formulaDepth_eq_zero_of_forall_eq {n : ℕ} {f : Cslib.BooleanFunction n} {b : Bool} (h : ∀ (x : Cslib.BitString n), f x = b) : formulaDepth f = 0

A constant function has formula depth 0.

theorem Algebraic.KW.one_le_formulaSize {n : ℕ} (f : Cslib.BooleanFunction n) : 1 ≤ formulaSize f

Every formula has a leaf, so every formula size is at least 1.

theorem Algebraic.KW.formulaSize_eq_one_of_forall_eq {n : ℕ} {f : Cslib.BooleanFunction n} {b : Bool} (h : ∀ (x : Cslib.BitString n), f x = b) : formulaSize f = 1

A constant function has formula size 1.

theorem Algebraic.KW.formulaDepth_outer_le_compose_of_nonConstant {m n : ℕ} {f : Cslib.BooleanFunction m} {g : Cslib.BooleanFunction n} (hg : NonConstant g) : formulaDepth f ≤ formulaDepth (compose f g)

For non-constant g, the depth of f is at most the depth of f ⋄ g.

theorem Algebraic.KW.formulaDepth_inner_le_compose_of_nonConstant {m n : ℕ} {f : Cslib.BooleanFunction m} {g : Cslib.BooleanFunction n} (hf : NonConstant f) : formulaDepth g ≤ formulaDepth (compose f g)

For non-constant f, the depth of g is at most the depth of f ⋄ g.

The conjecture

def Algebraic.KW.KRWDepthWith (c : ℕ) : Prop

The Karchmer–Raz–Wigderson conjecture, depth form, with additive slack c: for all non-constant f on m bits and g on n bits, formulaDepth f + formulaDepth g ≤ formulaDepth (f ⋄ g) + c. The slack c is a single number, independent of m, n, f and g. The converse inequality formulaDepth (f ⋄ g) ≤ formulaDepth f + formulaDepth g holds for all f and g (formulaDepth_compose_le).

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.KW.KRWSizeWith (c : ℕ) : Prop

The Karchmer–Raz–Wigderson conjecture, size form, with multiplicative slack c: for all non-constant f on m bits and g on n bits, formulaSize f * formulaSize g ≤ c * formulaSize (f ⋄ g). The slack c is a single number, independent of m, n, f and g. The converse inequality formulaSize (f ⋄ g) ≤ formulaSize f * formulaSize g holds for all f and g (formulaSize_compose_le).

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.KW.KRWDepth : Prop

The KRW conjecture, depth form (open): some constant additive slack works, ∃ c, KRWDepthWith c.

Equations

• Algebraic.KW.KRWDepth = ∃ (c : ℕ), Algebraic.KW.KRWDepthWith c

def Algebraic.KW.KRWSize : Prop

The KRW conjecture, size form (open): some constant multiplicative slack works, ∃ c, KRWSizeWith c.

Equations

• Algebraic.KW.KRWSize = ∃ (c : ℕ), Algebraic.KW.KRWSizeWith c

theorem Algebraic.KW.KRWDepthWith.mono {c c' : ℕ} (h : KRWDepthWith c) (hc : c ≤ c') : KRWDepthWith c'

A larger additive slack gives a weaker statement.

theorem Algebraic.KW.KRWSizeWith.mono {c c' : ℕ} (h : KRWSizeWith c) (hc : c ≤ c') : KRWSizeWith c'

A larger multiplicative slack gives a weaker statement.

Both non-constancy hypotheses are needed

If f or g is constant then f ⋄ g is constant, of depth 0 and size 1, while the other function can have depth or size above any fixed slack. So dropping either hypothesis from KRWDepthWith c or KRWSizeWith c gives a false statement, whatever c is. The witness of large depth and size is the conjunction of all k bits, whose formulas read every bit and so have at least k leaves and depth at least log₂ k.

def Algebraic.KW.Formula.vars {n : ℕ} : Formula n → Finset (Fin n)

The coordinates read by some literal of a formula.

Equations

• (Algebraic.KW.Formula.lit i b).vars = {i}
• (Algebraic.KW.Formula.const b).vars = ∅
• (l.and r).vars = l.vars ∪ r.vars
• (l.or r).vars = l.vars ∪ r.vars

theorem Algebraic.KW.Formula.card_vars_le_leaves {n : ℕ} (F : Formula n) : F.vars.card ≤ F.leaves

theorem Algebraic.KW.Formula.eval_update_of_notMem_vars {n : ℕ} {i : Fin n} (b : Bool) (x : Fin n → Bool) (F : Formula n) : i ∉ F.vars → F.eval (Function.update x i b) = F.eval x

Changing a coordinate that a formula does not read leaves its value unchanged.

theorem Algebraic.KW.Formula.mem_vars_of_computes {n : ℕ} {F : Formula n} {f : Cslib.BooleanFunction n} (hF : F.Computes f) {i : Fin n} {a : Fin n → Bool} (h : f (Function.update a i true) ≠ f (Function.update a i false)) : i ∈ F.vars

A formula reads every coordinate its function is sensitive to.

theorem Algebraic.KW.Formula.leaves_le_two_pow_depth {n : ℕ} (F : Formula n) : F.leaves ≤ 2 ^ F.depth

theorem Algebraic.KW.not_forall_depth_of_constant_inner (c : ℕ) : ¬∀ (m n : ℕ) (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n), NonConstant f → formulaDepth f + formulaDepth g ≤ formulaDepth (compose f g) + ↑c

Without non-constancy of g, the depth form fails for every slack c.

theorem Algebraic.KW.not_forall_depth_of_constant_outer (c : ℕ) : ¬∀ (m n : ℕ) (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n), NonConstant g → formulaDepth f + formulaDepth g ≤ formulaDepth (compose f g) + ↑c

Without non-constancy of f, the depth form fails for every slack c.

theorem Algebraic.KW.not_forall_size_of_constant_inner (c : ℕ) : ¬∀ (m n : ℕ) (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n), NonConstant f → formulaSize f * formulaSize g ≤ ↑c * formulaSize (compose f g)

Without non-constancy of g, the size form fails for every slack c.

theorem Algebraic.KW.not_forall_size_of_constant_outer (c : ℕ) : ¬∀ (m n : ℕ) (f : Cslib.BooleanFunction m) (g : Cslib.BooleanFunction n), NonConstant g → formulaSize f * formulaSize g ≤ ↑c * formulaSize (compose f g)

Without non-constancy of f, the size form fails for every slack c.