Unrestricted depth-three lower bound: circuit

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/Circuit.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.DepthThreeLowerBound.GateInput.subst {V : Type uDepth1} {W : Type uDepth2} (s : V → W ⊕ Bool) : GateInput V → GateInput W

Substitute variables or constants into a gate input, respecting literal signs.

Equations

• Complexity.DepthThreeLowerBound.GateInput.subst s (Sum.inl (v, b)) = match s v with | Sum.inl w => Sum.inl (w, b) | Sum.inr c => Sum.inr (decide (c = b))
• Complexity.DepthThreeLowerBound.GateInput.subst s (Sum.inr b) = Sum.inr b

def Complexity.DepthThreeLowerBound.GateInput.assignment {V : Type uDepth1} {W : Type uDepth2} (s : V → W ⊕ Bool) (x : Cube W) : Cube V

Lift an assignment through a variable-or-constant substitution.

Equations

• Complexity.DepthThreeLowerBound.GateInput.assignment s x v = match s v with | Sum.inl w => x w | Sum.inr b => b

@[simp]

theorem Complexity.DepthThreeLowerBound.GateInput.eval_subst {V : Type uDepth1} {W : Type uDepth2} (s : V → W ⊕ Bool) (l : GateInput V) (x : Cube W) : (subst s l).eval x = l.eval (assignment s x)

@[simp]

theorem Complexity.DepthThreeLowerBound.RawClause.eval_eq_true {V : Type uDepth1} (C : RawClause V) (x : Cube V) : C.eval x = true ↔ ∃ l ∈ C, l.eval x = true

@[simp]

theorem Complexity.DepthThreeLowerBound.RawClause.eval_map_subst {V : Type uDepth1} {W : Type uDepth2} (s : V → W ⊕ Bool) (C : RawClause V) (x : Cube W) : eval (List.map (GateInput.subst s) C) x = C.eval (GateInput.assignment s x)

@[simp]

theorem Complexity.DepthThreeLowerBound.Circuit3.middleEval_eq_true {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) (x : Cube V) : C.middleEval j x = true ↔ ∀ i ∈ C.middle j, (C.bottom i).eval x = true

@[simp]

theorem Complexity.DepthThreeLowerBound.Circuit3.eval_eq_true {V : Type uDepth1} (C : Circuit3 V) (x : Cube V) : C.eval x = true ↔ ∃ j ∈ C.top, C.middleEval j x = true

theorem Complexity.DepthThreeLowerBound.Circuit3.bottomCount_le_gateCount {V : Type uDepth1} (C : Circuit3 V) : C.bottomCount ≤ C.gateCount

theorem Complexity.DepthThreeLowerBound.Circuit3.middleCount_le_gateCount {V : Type uDepth1} (C : Circuit3 V) : C.middleCount ≤ C.gateCount

theorem Complexity.DepthThreeLowerBound.Circuit3.middle_card_le_gateCount {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) : (C.middle j).card ≤ C.gateCount

theorem Complexity.DepthThreeLowerBound.Circuit3.top_card_le_gateCount {V : Type uDepth1} (C : Circuit3 V) : C.top.card ≤ C.gateCount

def Complexity.DepthThreeLowerBound.Circuit3.subst {V : Type uDepth1} {W : Type uDepth2} (C : Circuit3 V) (s : V → W ⊕ Bool) : Circuit3 W

Apply an input substitution to every bottom clause, preserving all gates.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.Circuit3.gateCount_subst {V : Type uDepth1} {W : Type uDepth2} (C : Circuit3 V) (s : V → W ⊕ Bool) : (C.subst s).gateCount = C.gateCount

@[simp]

theorem Complexity.DepthThreeLowerBound.Circuit3.middleEval_subst {V : Type uDepth1} {W : Type uDepth2} (C : Circuit3 V) (s : V → W ⊕ Bool) (j : Fin C.middleCount) (x : Cube W) : (C.subst s).middleEval j x = C.middleEval j (GateInput.assignment s x)

@[simp]

theorem Complexity.DepthThreeLowerBound.Circuit3.eval_subst {V : Type uDepth1} {W : Type uDepth2} (C : Circuit3 V) (s : V → W ⊕ Bool) (x : Cube W) : (C.subst s).eval x = C.eval (GateInput.assignment s x)

theorem Complexity.DepthThreeLowerBound.Circuit3.computes_subst {V : Type uDepth1} {W : Type uDepth2} (C : Circuit3 V) {f : Cube V → Bool} (h : C.Computes f) (s : V → W ⊕ Bool) : (C.subst s).Computes fun (x : Cube W) => f (GateInput.assignment s x)