Unrestricted depth-three lower bound: restriction easy base

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

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

noncomputable def Complexity.DepthThreeLowerBound.indexedCNF {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (C : I → Clause V) : CNF V

Convert an indexed clause family into a CNF list.

Equations

• Complexity.DepthThreeLowerBound.indexedCNF C = List.map C Finset.univ.toList

theorem Complexity.DepthThreeLowerBound.indexedCNF_eval_eq_true {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (C : I → Clause V) (x : Cube V) : (indexedCNF C).eval x = true ↔ ∀ (i : I), (C i).eval x = true

theorem Complexity.DepthThreeLowerBound.clauseViolationCount_zero_iff {V : Type uDepth1} {I : Type uDepth2} (C : I → Clause V) (x : Cube V) (S : Finset I) : {i ∈ S | (C i).violation x = true}.card = 0 ↔ ∀ i ∈ S, (C i).eval x = true

theorem Complexity.DepthThreeLowerBound.indexedCNF_eval_indicator {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (C : I → Clause V) (x : Cube V) : indicator ((indexedCNF C).eval x) = if (totalCount fun (i : I) => (C i).violation x) = 0 then 1 else 0

noncomputable def Complexity.DepthThreeLowerBound.easyBaseIndices {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : Finset I

Indices of the easy clauses retained in the base factor.

Equations

• Complexity.DepthThreeLowerBound.easyBaseIndices C b σ = {i : I | ((C i).scope ∩ Complexity.DepthThreeLowerBound.liveSet σ).card ≤ b}

noncomputable def Complexity.DepthThreeLowerBound.easyBaseClause {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (i : I) : Option (Clause (Live σ))

The clause contributed by one easy-base index.

Equations

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

theorem Complexity.DepthThreeLowerBound.easyBaseClause_eval {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (i : I) (x : Cube (Live σ)) : residualClauseEval (easyBaseClause C σ i) x = (C i).eval (fill σ x)

noncomputable def Complexity.DepthThreeLowerBound.easyBaseCNF {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : CNF (Live σ)

The CNF formed by the easy-base clauses.

Equations

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

theorem Complexity.DepthThreeLowerBound.easyBaseCNF_widthAtMost {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : (easyBaseCNF C b σ).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.easyBaseCNF_eval_iff_all {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (x : Cube (Live σ)) : (easyBaseCNF C b σ).eval x = true ↔ ∀ i ∈ easyBaseIndices C b σ, (C i).eval (fill σ x) = true

theorem Complexity.DepthThreeLowerBound.easyBaseCNF_eval_eq_true {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (x : Cube (Live σ)) : (easyBaseCNF C b σ).eval x = true ↔ easyCount (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) ∅ = 0

theorem Complexity.DepthThreeLowerBound.easyBaseCNF_eval_indicator {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (x : Cube (Live σ)) : indicator ((easyBaseCNF C b σ).eval x) = if easyCount (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) ∅ = 0 then 1 else 0

def Complexity.DepthThreeLowerBound.cnfIndexFamily {V : Type uDepth1} (H : CNF V) (i : Fin (List.length H)) : Clause V

View a CNF list as a clause family indexed by its positions.

Equations

• Complexity.DepthThreeLowerBound.cnfIndexFamily H i = List.get H i

theorem Complexity.DepthThreeLowerBound.cnfIndexFamily_normalized {V : Type uDepth1} {H : CNF V} (hH : H.Normalized) (i : Fin (List.length H)) : (cnfIndexFamily H i).Normalized

theorem Complexity.DepthThreeLowerBound.cnfIndexFamily_width {V : Type uDepth1} {H : CNF V} {k : ℕ} (hH : H.WidthAtMost k) (i : Fin (List.length H)) : (cnfIndexFamily H i).width ≤ k

@[simp]

theorem Complexity.DepthThreeLowerBound.indexedCNF_cnfIndexFamily_eval {V : Type uDepth1} (H : CNF V) (x : Cube V) : (indexedCNF (cnfIndexFamily H)).eval x = H.eval x