Unrestricted depth-three lower bound: restriction clause

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionClause.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.liveClause {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Clause V) : Clause (Live σ)

The live literals of a clause under a restriction.

Equations

• Complexity.DepthThreeLowerBound.liveClause σ C = {l : Complexity.DepthThreeLowerBound.Literal (Complexity.DepthThreeLowerBound.Live σ) | (↑l.1, l.2) ∈ C}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_liveClause {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Clause V) (l : Literal (Live σ)) : l ∈ liveClause σ C ↔ (↑l.1, l.2) ∈ C

theorem Complexity.DepthThreeLowerBound.liveClause_scope_image_subset {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Clause V) : Finset.image Subtype.val (liveClause σ C).scope ⊆ C.scope

theorem Complexity.DepthThreeLowerBound.liveClause_width_le {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Clause V) : (liveClause σ C).width ≤ C.width

theorem Complexity.DepthThreeLowerBound.liveClause_normalized {V : Type uDepth1} [Fintype V] (σ : Restriction V) {C : Clause V} (hC : C.Normalized) : (liveClause σ C).Normalized

noncomputable def Complexity.DepthThreeLowerBound.restrictClause {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Clause V) : Option (Clause (Live σ))

Simplify a clause after fixing the restricted coordinates.

Equations

• Complexity.DepthThreeLowerBound.restrictClause σ C = if ∃ l ∈ C, σ l.1 = some l.2 then none else some (Complexity.DepthThreeLowerBound.liveClause σ C)

noncomputable def Complexity.DepthThreeLowerBound.residualClauseEval {W : Type uDepth2} (C : Option (Clause W)) (x : Cube W) : Bool

Evaluate the remaining part of a clause on its live variables.

Equations

• Complexity.DepthThreeLowerBound.residualClauseEval none x = true
• Complexity.DepthThreeLowerBound.residualClauseEval (some C_2) x = C_2.eval x

@[simp]

theorem Complexity.DepthThreeLowerBound.residualClauseEval_none {W : Type uDepth3} (x : Cube W) : residualClauseEval none x = true

@[simp]

theorem Complexity.DepthThreeLowerBound.residualClauseEval_some {W : Type uDepth4} (C : Clause W) (x : Cube W) : residualClauseEval (some C) x = C.eval x

theorem Complexity.DepthThreeLowerBound.restrictClause_eval {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Clause V) (z : Cube (Live σ)) : residualClauseEval (restrictClause σ C) z = C.eval (fill σ z)

theorem Complexity.DepthThreeLowerBound.restrictClause_some_eq {V : Type uDepth1} [Fintype V] {σ : Restriction V} {C : Clause V} {D : Clause (Live σ)} (h : restrictClause σ C = some D) : D = liveClause σ C

theorem Complexity.DepthThreeLowerBound.restrictClause_width_le {V : Type uDepth1} [Fintype V] {σ : Restriction V} {C : Clause V} {D : Clause (Live σ)} (h : restrictClause σ C = some D) : D.width ≤ C.width

theorem Complexity.DepthThreeLowerBound.restrictClause_normalized {V : Type uDepth1} [Fintype V] {σ : Restriction V} {C : Clause V} {D : Clause (Live σ)} (hC : C.Normalized) (h : restrictClause σ C = some D) : D.Normalized

@[simp]

theorem Complexity.DepthThreeLowerBound.restrictClause_empty {V : Type uDepth1} [Fintype V] (σ : Restriction V) : restrictClause σ ∅ = some ∅

def Complexity.DepthThreeLowerBound.residualCNF {W : Type uDepth5} (H : List (Option (Clause W))) : CNF W

The conjunction of residual clauses after a restriction.

Equations

• Complexity.DepthThreeLowerBound.residualCNF H = List.filterMap id H

@[simp]

theorem Complexity.DepthThreeLowerBound.residualCNF_nil {W : Type uDepth6} : residualCNF [] = []

@[simp]

theorem Complexity.DepthThreeLowerBound.residualCNF_cons_none {W : Type uDepth7} (H : List (Option (Clause W))) : residualCNF (none :: H) = residualCNF H

@[simp]

theorem Complexity.DepthThreeLowerBound.residualCNF_cons_some {W : Type uDepth8} (C : Clause W) (H : List (Option (Clause W))) : residualCNF (some C :: H) = C :: residualCNF H

theorem Complexity.DepthThreeLowerBound.residualCNF_eval_cons {W : Type uDepth9} (C : Option (Clause W)) (H : List (Option (Clause W))) (x : Cube W) : (residualCNF (C :: H)).eval x = (residualClauseEval C x && (residualCNF H).eval x)

noncomputable def Complexity.DepthThreeLowerBound.restrictCNF {V : Type uDepth1} [Fintype V] (σ : Restriction V) (H : CNF V) : CNF (Live σ)

Apply a restriction to every clause in a CNF.

Equations

• Complexity.DepthThreeLowerBound.restrictCNF σ H = List.filterMap (Complexity.DepthThreeLowerBound.restrictClause σ) H

@[simp]

theorem Complexity.DepthThreeLowerBound.restrictCNF_eval {V : Type uDepth1} [Fintype V] (σ : Restriction V) (H : CNF V) (z : Cube (Live σ)) : (restrictCNF σ H).eval z = H.eval (fill σ z)

theorem Complexity.DepthThreeLowerBound.restrictCNF_widthAtMost {V : Type uDepth1} [Fintype V] (σ : Restriction V) {H : CNF V} {b : ℕ} (hH : H.WidthAtMost b) : (restrictCNF σ H).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.restrictCNF_normalized {V : Type uDepth1} [Fintype V] (σ : Restriction V) {H : CNF V} (hH : H.Normalized) : (restrictCNF σ H).Normalized