Finite connectives and depth-two synthesis

Constructing a new root adds one layer. Merging roots of the same kind uses list flattening and preserves depth. Every Boolean function has depth-two layers with at most 2^n + 1 gates, including at input length zero.

noncomputable def Complexity.Shallow.Layer.gate {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n d) : Layer n (d + 1)

One root gate over a finite family of child layers.

Equations

• Complexity.Shallow.Layer.gate fs = List.map fs Finset.univ.toList

theorem Complexity.Shallow.Layer.size_gate {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n d) : (gate fs).size = 1 + ∑ i : ι, (fs i).size

theorem Complexity.Shallow.Layer.eval_gate_and {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n d) (x : BitString n) : eval AndOrOp.and (gate fs) x = true ↔ ∀ (i : ι), eval AndOrOp.or (fs i) x = true

theorem Complexity.Shallow.Layer.eval_gate_or {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n d) (x : BitString n) : eval AndOrOp.or (gate fs) x = true ↔ ∃ (i : ι), eval AndOrOp.and (fs i) x = true

noncomputable def Complexity.Shallow.Layer.merge {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n (d + 1)) : Layer n (d + 1)

Merge a finite collection of roots without adding a layer.

Equations

• Complexity.Shallow.Layer.merge fs = (List.map fs Finset.univ.toList).flatten

theorem Complexity.Shallow.Layer.eval_merge_and {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n (d + 1)) (x : BitString n) : eval AndOrOp.and (merge fs) x = true ↔ ∀ (i : ι), eval AndOrOp.and (fs i) x = true

theorem Complexity.Shallow.Layer.eval_merge_or {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n (d + 1)) (x : BitString n) : eval AndOrOp.or (merge fs) x = true ↔ ∃ (i : ι), eval AndOrOp.or (fs i) x = true

theorem Complexity.Shallow.Layer.size_merge_le {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → Layer n (d + 1)) : (merge fs).size ≤ 1 + ∑ i : ι, (fs i).size

def Complexity.Shallow.Layer.constant (n d : ℕ) (op : AndOrOp) (b : Bool) : Layer n (d + 2)

A constant represented at any depth at least two.

Equations

• Complexity.Shallow.Layer.constant n d op b = if b = decide (op = Complexity.AndOrOp.and) then [] else [[]]

theorem Complexity.Shallow.Layer.eval_constant (n d : ℕ) (op : AndOrOp) (b : Bool) (x : BitString n) : eval op (constant n d op b) x = b

theorem Complexity.Shallow.Layer.size_constant_le (n d : ℕ) (op : AndOrOp) (b : Bool) : (constant n d op b).size ≤ 2

noncomputable def Complexity.Shallow.Layer.excludingClause {n : ℕ} (y : BitString n) : Layer n 1

A clause excluding precisely one assignment.

Equations

• Complexity.Shallow.Layer.excludingClause y = Complexity.Shallow.Layer.gate fun (i : Fin n) => (i, y i)

theorem Complexity.Shallow.Layer.eval_excludingClause {n : ℕ} (y x : BitString n) : eval AndOrOp.or (excludingClause y) x = true ↔ x ≠ y

theorem Complexity.Shallow.Layer.size_excludingClause {n : ℕ} (y : BitString n) : (excludingClause y).size = 1

noncomputable def Complexity.Shallow.Layer.cnf {n : ℕ} (f : BitString n → Bool) : Layer n 2

Truth-table CNF, used only at the bottom of the depth induction.

Equations

• Complexity.Shallow.Layer.cnf f = Complexity.Shallow.Layer.gate fun (y : { y : Complexity.BitString n // f y = false }) => Complexity.Shallow.Layer.excludingClause ↑y

theorem Complexity.Shallow.Layer.eval_cnf {n : ℕ} (f : BitString n → Bool) (x : BitString n) : eval AndOrOp.and (cnf f) x = f x

theorem Complexity.Shallow.Layer.size_cnf_le {n : ℕ} (f : BitString n → Bool) : (cnf f).size ≤ 2 ^ n + 1

theorem Complexity.Shallow.Layer.exists_depth_two {n : ℕ} (f : BitString n → Bool) (op : AndOrOp) : ∃ (g : Layer n 2), g.size ≤ 2 ^ n + 1 ∧ ∀ (x : BitString n), eval op g x = f x

Every Boolean function has AND-rooted and OR-rooted depth-two layers.