Unrestricted depth-three lower bound: restriction marker cnf

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

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

theorem Complexity.DepthThreeLowerBound.residualCNF_eval_eq_true {V : Type uDepth1} (L : List (Option (Clause V))) (x : Cube V) : (residualCNF L).eval x = true ↔ ∀ C ∈ L, residualClauseEval C x = true

theorem Complexity.DepthThreeLowerBound.residualCNF_widthAtMost {V : Type uDepth1} (L : List (Option (Clause V))) {b : ℕ} (h : ∀ (C : Clause V), some C ∈ L → C.width ≤ b) : (residualCNF L).WidthAtMost b

noncomputable def Complexity.DepthThreeLowerBound.markerCNF {V : Type uDepth1} {I : Type uDepth2} [Fintype I] (C : I → Option (Clause V)) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) : CNF V

The CNF corresponding to a single marker test.

Equations

• Complexity.DepthThreeLowerBound.markerCNF C c π = Complexity.DepthThreeLowerBound.residualCNF (List.map C (Complexity.DepthThreeLowerBound.markerSelected c π).toList)

@[simp]

theorem Complexity.DepthThreeLowerBound.markerCNF_eval {V : Type uDepth1} {I : Type uDepth2} [Fintype I] [instDecidableEqI : DecidableEq I] (C : I → Option (Clause V)) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) (x : Cube V) : (markerCNF C c π).eval x = markerSample (fun (i : I) (x : Cube V) => residualClauseEval (C i) x) c π x

theorem Complexity.DepthThreeLowerBound.markerCNF_widthAtMost {V : Type uDepth1} {I : Type uDepth2} [Fintype I] (C : I → Option (Clause V)) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) {b : ℕ} (h : ∀ (i : I) (D : Clause V), C i = some D → D.width ≤ b) : (markerCNF C c π).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.markerCNF_avg {V : Type uDepth1} {I : Type uDepth2} [Fintype I] [instDecidableEqI : DecidableEq I] (C : I → Option (Clause V)) {c : ℕ} (hc : 0 < c) (x : Cube V) : (finiteAvg fun (π : Equiv.Perm (I ⊕ Fin c)) => indicator ((markerCNF C c π).eval x)) = ↑c / (↑c + ↑(markerBad (fun (i : I) (x : Cube V) => residualClauseEval (C i) x) x).card)

noncomputable def Complexity.DepthThreeLowerBound.markerProductCNF {V : Type uDepth1} {H : Type uDepth3} [Fintype H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) : CNF V

The CNF corresponding to a product of marker tests.

Equations

• Complexity.DepthThreeLowerBound.markerProductCNF C c π = List.flatMap (fun (h : H) => Complexity.DepthThreeLowerBound.markerCNF (C h) (c h) (π h)) Finset.univ.toList

theorem Complexity.DepthThreeLowerBound.markerProductCNF_eval_eq_true {V : Type uDepth1} {H : Type uDepth3} [Fintype H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) (x : Cube V) : (markerProductCNF C c π).eval x = true ↔ ∀ (h : H), (markerCNF (C h) (c h) (π h)).eval x = true

theorem Complexity.DepthThreeLowerBound.markerProductCNF_indicator {V : Type uDepth1} {H : Type uDepth3} [Fintype H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) (x : Cube V) : indicator ((markerProductCNF C c π).eval x) = ∏ h : H, indicator ((markerCNF (C h) (c h) (π h)).eval x)

theorem Complexity.DepthThreeLowerBound.markerProductCNF_widthAtMost {V : Type uDepth1} {H : Type uDepth3} [Fintype H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) {b : ℕ} (hC : ∀ (h : H) (i : J h) (D : Clause V), C h i = some D → D.width ≤ b) : (markerProductCNF C c π).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.markerProductCNF_avg {V : Type uDepth1} {H : Type uDepth3} [Fintype H] [instDecidableEqH : DecidableEq H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] [insthDecidableEqJh : (h : H) → DecidableEq (J h)] (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (hc : ∀ (h : H), 0 < c h) (x : Cube V) : (finiteAvg fun (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) => indicator ((markerProductCNF C c π).eval x)) = ∏ h : H, ↑(c h) / (↑(c h) + ↑(markerBad (fun (i : J h) (x : Cube V) => residualClauseEval (C h i) x) x).card)

noncomputable def Complexity.DepthThreeLowerBound.markerCylinderCNF {V : Type uDepth1} {H : Type uDepth3} [Fintype H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] (K : CNF V) (U : Finset V) (pattern : Cube V) (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) : CNF V

Combine marker tests with the path's fixed-coordinate cylinder.

Equations

• Complexity.DepthThreeLowerBound.markerCylinderCNF K U pattern C c π = K ++ Complexity.DepthThreeLowerBound.cylinderCNF U pattern ++ Complexity.DepthThreeLowerBound.markerProductCNF C c π

theorem Complexity.DepthThreeLowerBound.markerCylinderCNF_widthAtMost {V : Type uDepth1} {H : Type uDepth3} [Fintype H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] (K : CNF V) (U : Finset V) (pattern : Cube V) (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) {b : ℕ} (hb : 1 ≤ b) (hK : K.WidthAtMost b) (hC : ∀ (h : H) (i : J h) (D : Clause V), C h i = some D → D.width ≤ b) : (markerCylinderCNF K U pattern C c π).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.markerCylinderCNF_avg {V : Type uDepth1} {H : Type uDepth3} [Fintype H] [instDecidableEqH : DecidableEq H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] [insthDecidableEqJh : (h : H) → DecidableEq (J h)] (K : CNF V) (U : Finset V) (pattern x : Cube V) (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (hc : ∀ (h : H), 0 < c h) : (finiteAvg fun (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) => indicator ((markerCylinderCNF K U pattern C c π).eval x)) = indicator (K.eval x) * indicator ((cylinderCNF U pattern).eval x) * ∏ h : H, ↑(c h) / (↑(c h) + ↑(markerBad (fun (i : J h) (x : Cube V) => residualClauseEval (C h i) x) x).card)

theorem Complexity.DepthThreeLowerBound.markerCylinderCNF_scaled_avg {V : Type uDepth1} {H : Type uDepth3} [Fintype H] [instDecidableEqH : DecidableEq H] {J : H → Type uDepth4} [(h : H) → Fintype (J h)] [insthDecidableEqJh : (h : H) → DecidableEq (J h)] (K : CNF V) (U : Finset V) (pattern x : Cube V) (C : (h : H) → J h → Option (Clause V)) (c : H → ℕ) (hc : ∀ (h : H), 0 < c h) : ((∏ h : H, (↑(c h))⁻¹) * finiteAvg fun (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) => indicator ((markerCylinderCNF K U pattern C c π).eval x)) = indicator (K.eval x) * indicator ((cylinderCNF U pattern).eval x) * ∏ h : H, (↑(c h) + ↑(markerBad (fun (i : J h) (x : Cube V) => residualClauseEval (C h i) x) x).card)⁻¹