Unrestricted depth-three lower bound: sparse counting

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

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

def Complexity.DepthThreeLowerBound.clausesOfSize {V : Type uDepth1} (A : Finset (Clause V)) (u : ℕ) : Finset (Clause V)

Clauses in the family with the specified cardinality.

Equations

• Complexity.DepthThreeLowerBound.clausesOfSize A u = {C ∈ A | Finset.card C = u}

def Complexity.DepthThreeLowerBound.literalOccurrences {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A : Finset (Clause V)) (u : ℕ) (l : Literal V) : ℕ

Count clauses of the specified size containing a literal.

Equations

• Complexity.DepthThreeLowerBound.literalOccurrences A u l = {C ∈ Complexity.DepthThreeLowerBound.clausesOfSize A u | l ∈ C}.card

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_clausesOfSize {V : Type uDepth1} {A : Finset (Clause V)} {u : ℕ} {C : Clause V} : C ∈ clausesOfSize A u ↔ C ∈ A ∧ Finset.card C = u

theorem Complexity.DepthThreeLowerBound.clausesOfSize_subset {V : Type uDepth1} (A : Finset (Clause V)) (u : ℕ) : clausesOfSize A u ⊆ A

theorem Complexity.DepthThreeLowerBound.clausesOfSize_mono {V : Type uDepth1} {A B : Finset (Clause V)} (h : A ⊆ B) (u : ℕ) : clausesOfSize A u ⊆ clausesOfSize B u

theorem Complexity.DepthThreeLowerBound.clausesOfSize_eq_self {V : Type uDepth1} (A : Finset (Clause V)) (u : ℕ) (h : ∀ C ∈ A, Finset.card C = u) : clausesOfSize A u = A

theorem Complexity.DepthThreeLowerBound.clausesOfSize_eq_empty {V : Type uDepth1} (A : Finset (Clause V)) (u : ℕ) (h : ∀ C ∈ A, Finset.card C ≠ u) : clausesOfSize A u = ∅

theorem Complexity.DepthThreeLowerBound.literalOccurrences_mono {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {A B : Finset (Clause V)} (h : A ⊆ B) (u : ℕ) (l : Literal V) : literalOccurrences A u l ≤ literalOccurrences B u l

theorem Complexity.DepthThreeLowerBound.literalOccurrences_le_card {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A : Finset (Clause V)) (u : ℕ) (l : Literal V) : literalOccurrences A u l ≤ (clausesOfSize A u).card

theorem Complexity.DepthThreeLowerBound.literalOccurrences_one_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A : Finset (Clause V)) (l : Literal V) : literalOccurrences A 1 l ≤ 1

theorem Complexity.DepthThreeLowerBound.clausesOfSize_union {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (u : ℕ) : clausesOfSize (A ∪ B) u = clausesOfSize A u ∪ clausesOfSize B u

theorem Complexity.DepthThreeLowerBound.literalOccurrences_union_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (u : ℕ) (l : Literal V) : literalOccurrences (A ∪ B) u l ≤ literalOccurrences A u l + literalOccurrences B u l

theorem Complexity.DepthThreeLowerBound.clausesOfSize_card_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] [Fintype V] (A : Finset (Clause V)) (u n : ℕ) (hne : ∀ C ∈ clausesOfSize A u, Finset.Nonempty C) (hocc : ∀ (l : Literal V), literalOccurrences A u l ≤ n) : (clausesOfSize A u).card ≤ 2 * Fintype.card V * n

theorem Complexity.DepthThreeLowerBound.subsumed_by_clause_card_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A : Finset (Clause V)) (u n : ℕ) (hocc : ∀ (l : Literal V), literalOccurrences A u l ≤ n) (D : Clause V) (hD : Finset.Nonempty D) : {C ∈ clausesOfSize A u | D ⊆ C}.card ≤ n

theorem Complexity.DepthThreeLowerBound.deleted_clausesOfSize_card_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B R : Finset (Clause V)) (u n : ℕ) (hne : ∀ D ∈ B, Finset.Nonempty D) (hocc : ∀ (l : Literal V), literalOccurrences A u l ≤ n) (hsub : R ⊆ clausesOfSize A u) (hcover : ∀ C ∈ R, ∃ D ∈ B, D ⊆ C) : R.card ≤ B.card * n

def Complexity.DepthThreeLowerBound.subsumedOfSize {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (u : ℕ) : Finset (Clause V)

Clauses of the specified size subsumed by the selected batch.

Equations

• Complexity.DepthThreeLowerBound.subsumedOfSize A B u = {C ∈ Complexity.DepthThreeLowerBound.clausesOfSize A u | ∃ D ∈ B, D ⊆ C}

theorem Complexity.DepthThreeLowerBound.subsumedOfSize_card_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (u n : ℕ) (hne : ∀ D ∈ B, Finset.Nonempty D) (hocc : ∀ (l : Literal V), literalOccurrences A u l ≤ n) : (subsumedOfSize A B u).card ≤ B.card * n

theorem Complexity.DepthThreeLowerBound.clausesOfSize_update_balance {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (u : ℕ) (hfresh : Disjoint A B) : (clausesOfSize (B ∪ {C ∈ A | ¬∃ D ∈ B, D ⊆ C}) u).card + (subsumedOfSize A B u).card = (clausesOfSize A u).card + (clausesOfSize B u).card

theorem Complexity.DepthThreeLowerBound.literalOccurrences_update_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (u : ℕ) (l : Literal V) : literalOccurrences (B ∪ {C ∈ A | ¬∃ D ∈ B, D ⊆ C}) u l ≤ literalOccurrences A u l + literalOccurrences B u l