Unrestricted depth-three lower bound: circuit normalization

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

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

def Complexity.DepthThreeLowerBound.RawClause.literalPart {V : Type uDepth1} : GateInput V → Option (Literal V)

Extract the literal inputs of a raw clause.

Equations

• Complexity.DepthThreeLowerBound.RawClause.literalPart (Sum.inl l) = some l
• Complexity.DepthThreeLowerBound.RawClause.literalPart (Sum.inr val) = none

noncomputable def Complexity.DepthThreeLowerBound.RawClause.literals {V : Type uDepth1} (C : RawClause V) : Clause V

The finite set of literals occurring in a raw clause.

Equations

• C.literals = (List.filterMap Complexity.DepthThreeLowerBound.RawClause.literalPart C).toFinset

@[simp]

theorem Complexity.DepthThreeLowerBound.RawClause.mem_literals {V : Type uDepth1} (C : RawClause V) (l : Literal V) : l ∈ C.literals ↔ Sum.inl l ∈ C

theorem Complexity.DepthThreeLowerBound.RawClause.eval_true_iff {V : Type uDepth1} (C : RawClause V) (x : Cube V) : C.eval x = true ↔ Sum.inr true ∈ C ∨ C.literals.eval x = true

noncomputable def Complexity.DepthThreeLowerBound.RawClause.normalize {V : Type uDepth1} (C : RawClause V) : Option (Clause V)

Normalize a raw clause, accounting for constants and complementary literals.

Equations

• C.normalize = if Sum.inr true ∈ C ∨ ¬C.literals.Normalized then none else some C.literals

theorem Complexity.DepthThreeLowerBound.RawClause.normalized_of_normalize_eq_some {V : Type uDepth1} {C : RawClause V} {D : Clause V} (h : C.normalize = some D) : D.Normalized

theorem Complexity.DepthThreeLowerBound.RawClause.normalize_eval {V : Type uDepth1} (C : RawClause V) (x : Cube V) : (Option.map (fun (D : Clause V) => D.eval x) C.normalize).getD true = C.eval x

noncomputable def Complexity.DepthThreeLowerBound.Circuit3.middleCNF {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) : CNF V

Represent a middle gate as the conjunction of its normalized bottom clauses.

Equations

• C.middleCNF j = List.filterMap (fun (i : Fin C.bottomCount) => (C.bottom i).normalize) (C.middle j).toList

theorem Complexity.DepthThreeLowerBound.Circuit3.mem_middleCNF {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) (D : Clause V) : D ∈ C.middleCNF j ↔ ∃ i ∈ C.middle j, (C.bottom i).normalize = some D

theorem Complexity.DepthThreeLowerBound.Circuit3.middleCNF_normalized {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) : (C.middleCNF j).Normalized

theorem Complexity.DepthThreeLowerBound.Circuit3.middleCNF_length_le_bottomCount {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) : List.length (C.middleCNF j) ≤ C.bottomCount

theorem Complexity.DepthThreeLowerBound.Circuit3.middleCNF_length_le_gateCount {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) : List.length (C.middleCNF j) ≤ C.gateCount

@[simp]

theorem Complexity.DepthThreeLowerBound.Circuit3.eval_middleCNF {V : Type uDepth1} (C : Circuit3 V) (j : Fin C.middleCount) (x : Cube V) : (C.middleCNF j).eval x = C.middleEval j x

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

theorem Complexity.DepthThreeLowerBound.Circuit3.middleCNF_implies_output {V : Type uDepth1} (C : Circuit3 V) {j : Fin C.middleCount} (hj : j ∈ C.top) {x : Cube V} (hx : (C.middleCNF j).eval x = true) : C.eval x = true