Unrestricted depth-three lower bound: sparse normalize

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/SparseNormalize.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_of_not_normalized {V : Type uDepth1} {C : Clause V} (hC : ¬C.Normalized) (x : Cube V) : C.eval x = true

theorem Complexity.DepthThreeLowerBound.CNF.eval_of_empty_mem {V : Type uDepth1} {H : CNF V} (hH : ∅ ∈ H) (x : Cube V) : H.eval x = false

noncomputable def Complexity.DepthThreeLowerBound.sparseNormalizedFamily {V : Type uDepth1} (H : CNF V) : Finset (Clause V)

Normalize a CNF into its finite family of minimal clauses.

Equations

• Complexity.DepthThreeLowerBound.sparseNormalizedFamily H = Finset.filter Complexity.DepthThreeLowerBound.Clause.Normalized (List.toFinset H)

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

theorem Complexity.DepthThreeLowerBound.sparseNormalizedFamily_eval {V : Type uDepth1} (H : CNF V) (x : Cube V) : CNF.eval (sparseNormalizedFamily H).toList x = H.eval x

theorem Complexity.DepthThreeLowerBound.sparseMinimalFamily_eval {V : Type uDepth1} (A : Finset (Clause V)) (x : Cube V) : CNF.eval (sparseMinimalFamily A).toList x = CNF.eval A.toList x

structure Complexity.DepthThreeLowerBound.SparseNormalization {V : Type uDepth1} (H : CNF V) (b : ℕ) : Type uDepth1

A normalized clause family with its width and semantic guarantees.

• active : Finset (Clause V)

  The currently active clauses.

• normalized (C : Clause V) : C ∈ self.active → C.Normalized
• nonempty (C : Clause V) : C ∈ self.active → Finset.Nonempty C
• antichain (C : Clause V) : C ∈ self.active → ∀ D ∈ self.active, C ⊆ D → C = D
• width_le (C : Clause V) : C ∈ self.active → C.width ≤ b
• eval_eq (x : Cube V) : CNF.eval self.active.toList x = H.eval x

noncomputable def Complexity.DepthThreeLowerBound.sparseNormalizeOfNoEmpty {V : Type uDepth1} (H : CNF V) {b : ℕ} (hwidth : H.WidthAtMost b) (hempty : ∅ ∉ H) : SparseNormalization H b

Normalize a CNF that contains no empty clause.

Equations

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

theorem Complexity.DepthThreeLowerBound.exists_sparseNormalization_or_false {V : Type uDepth1} (H : CNF V) {b : ℕ} (hwidth : H.WidthAtMost b) : (∀ (x : Cube V), H.eval x = false) ∨ Nonempty (SparseNormalization H b)