Unrestricted depth-three lower bound: restriction keep clause

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionKeepClause.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.keptLiterals {V : Type uDepth1} (R : Finset V) (C : Clause V) : Clause V

Literals retained by the specified coordinate selection.

Equations

• Complexity.DepthThreeLowerBound.keptLiterals R C = {l ∈ C | l.1 ∈ R}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_keptLiterals {V : Type uDepth1} (R : Finset V) (C : Clause V) (l : Literal V) : l ∈ keptLiterals R C ↔ l ∈ C ∧ l.1 ∈ R

theorem Complexity.DepthThreeLowerBound.keptLiterals_scope {V : Type uDepth1} (R : Finset V) (C : Clause V) : (keptLiterals R C).scope = C.scope ∩ R

theorem Complexity.DepthThreeLowerBound.keptLiterals_width {V : Type uDepth1} (R : Finset V) (C : Clause V) : (keptLiterals R C).width = (C.scope ∩ R).card

noncomputable def Complexity.DepthThreeLowerBound.keepClause {V : Type uDepth1} (R : Finset V) (pattern : Cube V) (C : Clause V) : Option (Clause V)

Retain the selected literals of a clause.

Equations

• Complexity.DepthThreeLowerBound.keepClause R pattern C = if ∃ l ∈ C, l.1 ∉ R ∧ pattern l.1 = l.2 then none else some (Complexity.DepthThreeLowerBound.keptLiterals R C)

theorem Complexity.DepthThreeLowerBound.keepClause_eval {V : Type uDepth1} (R : Finset V) (pattern x : Cube V) (C : Clause V) (hagree : ∀ v ∉ R, x v = pattern v) : residualClauseEval (keepClause R pattern C) x = C.eval x

theorem Complexity.DepthThreeLowerBound.keepClause_some_eq {V : Type uDepth1} {R : Finset V} {pattern : Cube V} {C D : Clause V} (h : keepClause R pattern C = some D) : D = keptLiterals R C

theorem Complexity.DepthThreeLowerBound.keepClause_width {V : Type uDepth1} {R : Finset V} {pattern : Cube V} {C D : Clause V} (h : keepClause R pattern C = some D) : D.width = (C.scope ∩ R).card

theorem Complexity.DepthThreeLowerBound.keepClause_normalized {V : Type uDepth1} {R : Finset V} {pattern : Cube V} {C D : Clause V} (hC : C.Normalized) (h : keepClause R pattern C = some D) : D.Normalized

noncomputable def Complexity.DepthThreeLowerBound.keptRestrictedClause {V : Type uDepth1} [Fintype V] (σ : Restriction V) (R : Finset V) (pattern : Cube V) (C : Clause V) : Option (Clause (Live σ))

Retain selected literals after applying a restriction.

Equations

• Complexity.DepthThreeLowerBound.keptRestrictedClause σ R pattern C = (Complexity.DepthThreeLowerBound.keepClause R pattern C).bind (Complexity.DepthThreeLowerBound.restrictClause σ)

theorem Complexity.DepthThreeLowerBound.residualClauseEval_bind_restrict {V : Type uDepth1} [Fintype V] (σ : Restriction V) (C : Option (Clause V)) (x : Cube (Live σ)) : residualClauseEval (C.bind (restrictClause σ)) x = residualClauseEval C (fill σ x)

theorem Complexity.DepthThreeLowerBound.keptRestrictedClause_eval {V : Type uDepth1} [Fintype V] (σ : Restriction V) (R : Finset V) (pattern : Cube V) (C : Clause V) (x : Cube (Live σ)) (hagree : ∀ v ∉ R, fill σ x v = pattern v) : residualClauseEval (keptRestrictedClause σ R pattern C) x = C.eval (fill σ x)

theorem Complexity.DepthThreeLowerBound.keptRestrictedClause_width_le {V : Type uDepth1} [Fintype V] {σ : Restriction V} {R : Finset V} {pattern : Cube V} {C : Clause V} {D : Clause (Live σ)} (h : keptRestrictedClause σ R pattern C = some D) : D.width ≤ (C.scope ∩ R).card