Unrestricted depth-three lower bound: restriction normalization

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

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

theorem Complexity.DepthThreeLowerBound.Clause.eval_true_of_not_normalized {V : Type uDepth1} {C : Clause V} (h : ¬C.Normalized) (x : Cube V) : C.eval x = true

noncomputable def Complexity.DepthThreeLowerBound.Clause.forbiddenValue {V : Type uDepth1} (C : Clause V) (v : V) : Bool

The value that falsifies the selected literal of a normalized clause.

Equations

• C.forbiddenValue v = decide ((v, false) ∈ C)

theorem Complexity.DepthThreeLowerBound.Clause.forbiddenValue_ne_literal {V : Type uDepth1} {C : Clause V} (hC : C.Normalized) {l : Literal V} (hl : l ∈ C) : C.forbiddenValue l.1 ≠ l.2

theorem Complexity.DepthThreeLowerBound.Clause.eval_eq_false_iff {V : Type uDepth1} (C : Clause V) (x : Cube V) : C.eval x = false ↔ ∀ l ∈ C, x l.1 ≠ l.2

theorem Complexity.DepthThreeLowerBound.Clause.eval_eq_false_iff_forbidden {V : Type uDepth1} {C : Clause V} (hC : C.Normalized) (x : Cube V) : C.eval x = false ↔ ∀ v ∈ C.scope, x v = C.forbiddenValue v

noncomputable def Complexity.DepthThreeLowerBound.Clause.violation {V : Type uDepth1} (C : Clause V) (x : Cube V) : Bool

The Boolean negation of a clause's evaluation.

Equations

• C.violation x = !C.eval x

@[simp]

theorem Complexity.DepthThreeLowerBound.Clause.violation_eq_true {V : Type uDepth1} (C : Clause V) (x : Cube V) : C.violation x = true ↔ C.eval x = false

theorem Complexity.DepthThreeLowerBound.Clause.violation_eq_true_iff_forbidden {V : Type uDepth1} {C : Clause V} (hC : C.Normalized) (x : Cube V) : C.violation x = true ↔ ∀ v ∈ C.scope, x v = C.forbiddenValue v

noncomputable def Complexity.DepthThreeLowerBound.CNF.normalize {V : Type uDepth1} (H : CNF V) : CNF V

Discard tautological clauses from a CNF.

Equations

• H.normalize = List.filter (fun (C : Complexity.DepthThreeLowerBound.Clause V) => decide C.Normalized) H

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.mem_normalize {V : Type uDepth1} {H : CNF V} {C : Clause V} : C ∈ H.normalize ↔ C ∈ H ∧ C.Normalized

theorem Complexity.DepthThreeLowerBound.CNF.normalize_normalized {V : Type uDepth1} (H : CNF V) : H.normalize.Normalized

theorem Complexity.DepthThreeLowerBound.CNF.normalize_widthAtMost {V : Type uDepth1} {H : CNF V} {b : ℕ} (hH : H.WidthAtMost b) : H.normalize.WidthAtMost b

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.eval_normalize {V : Type uDepth1} (H : CNF V) (x : Cube V) : H.normalize.eval x = H.eval x