Unrestricted depth-three lower bound: restriction cylinders

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionCylinders.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_eq_of_scope_agree {V : Type uDepth1} (C : Clause V) (x y : Cube V) (h : ∀ v ∈ C.scope, x v = y v) : C.eval x = C.eval y

theorem Complexity.DepthThreeLowerBound.Clause.violation_eq_of_scope_agree {V : Type uDepth1} (C : Clause V) (x y : Cube V) (h : ∀ v ∈ C.scope, x v = y v) : C.violation x = C.violation y

theorem Complexity.DepthThreeLowerBound.simultaneous_violation_iff_cylinder {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [instDecidableEqI : DecidableEq I] (C : I → Clause V) (T : Finset V) (P : List I) (x y : Cube V) (hn : ∀ i ∈ P, (C i).Normalized) (hy : ∀ i ∈ P, (C i).violation y = true) (hout : ∀ v ∉ T, x v = y v) : (∀ i ∈ P, (C i).violation x = true) ↔ ∀ v ∈ revealed (fun (i : I) => (C i).scope) T P, x v = y v

theorem Complexity.DepthThreeLowerBound.violation_eq_of_covered {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] (C : I → Clause V) (T U : Finset V) (x y : Cube V) (i : I) (hc : residual (fun (i : I) => (C i).scope) T U i = ∅) (hU : ∀ v ∈ U, x v = y v) (hout : ∀ v ∉ T, x v = y v) : (C i).violation x = (C i).violation y

theorem Complexity.DepthThreeLowerBound.coveredCount_eq_of_agree {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [instFintypeI : Fintype I] (C : I → Clause V) (T U : Finset V) (x y : Cube V) (hU : ∀ v ∈ U, x v = y v) (hout : ∀ v ∉ T, x v = y v) : coveredCount (fun (i : I) => (C i).scope) T (fun (i : I) => (C i).violation x) U = coveredCount (fun (i : I) => (C i).scope) T (fun (i : I) => (C i).violation y) U

theorem Complexity.DepthThreeLowerBound.coveredCount_eq_on_larger_cylinder {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [instFintypeI : Fintype I] (C : I → Clause V) (T U Z : Finset V) (x y : Cube V) (hUZ : U ⊆ Z) (hZ : ∀ v ∈ Z, x v = y v) (hout : ∀ v ∉ T, x v = y v) : coveredCount (fun (i : I) => (C i).scope) T (fun (i : I) => (C i).violation x) U = coveredCount (fun (i : I) => (C i).scope) T (fun (i : I) => (C i).violation y) U

noncomputable def Complexity.DepthThreeLowerBound.cylinderCNF {V : Type uDepth1} (U : Finset V) (pattern : Cube V) : CNF V

Express a fixed-coordinate cylinder as a CNF.

Equations

• Complexity.DepthThreeLowerBound.cylinderCNF U pattern = List.map (fun (v : V) => {(v, pattern v)}) U.toList

theorem Complexity.DepthThreeLowerBound.cylinderCNF_eval_eq_true {V : Type uDepth1} (U : Finset V) (pattern x : Cube V) : (cylinderCNF U pattern).eval x = true ↔ ∀ v ∈ U, x v = pattern v

theorem Complexity.DepthThreeLowerBound.cylinderCNF_eval {V : Type uDepth1} (U : Finset V) (pattern x : Cube V) : (cylinderCNF U pattern).eval x = decide (∀ v ∈ U, x v = pattern v)

theorem Complexity.DepthThreeLowerBound.cylinderCNF_widthAtMost {V : Type uDepth1} (U : Finset V) (pattern : Cube V) {b : ℕ} (hb : 1 ≤ b) : (cylinderCNF U pattern).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.cylinderCNF_normalized {V : Type uDepth1} (U : Finset V) (pattern : Cube V) : (cylinderCNF U pattern).Normalized

theorem Complexity.DepthThreeLowerBound.fill_agree_outside_live {V : Type uDepth1} (σ : Restriction V) (x y : Cube (Live σ)) (v : V) (hv : σ v ≠ none) : fill σ x v = fill σ y v

theorem Complexity.DepthThreeLowerBound.simultaneous_restricted_violation_iff {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [instDecidableEqI : DecidableEq I] (C : I → Clause V) (σ : Restriction V) (T : Finset V) (hT : ∀ (v : V), v ∈ T ↔ σ v = none) (P : List I) (x y : Cube (Live σ)) (hn : ∀ i ∈ P, (C i).Normalized) (hy : ∀ i ∈ P, (C i).violation (fill σ y) = true) : (∀ i ∈ P, (C i).violation (fill σ x) = true) ↔ ∀ v ∈ revealed (fun (i : I) => (C i).scope) T P, fill σ x v = fill σ y v