Unrestricted depth-three lower bound: restriction path mixture

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionPathMixture.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.pathIntermediateIndices {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (h : Fin P.length) : Finset I

Intermediate clause indices associated with a path prefix.

Equations

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

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.PathIntermediateIndex {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (h : Fin P.length) : Type uDepth2

An intermediate index together with its path position.

Equations

• Complexity.DepthThreeLowerBound.PathIntermediateIndex C b σ P h = ↥(Complexity.DepthThreeLowerBound.pathIntermediateIndices C b σ P h)

noncomputable def Complexity.DepthThreeLowerBound.pathReducedClause {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (h : Fin P.length) (i : PathIntermediateIndex C b σ P h) : Option (Clause (Live σ))

The residual clause associated with a path's intermediate index.

Equations

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

theorem Complexity.DepthThreeLowerBound.pathReducedClause_widthAtMost {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (h : Fin P.length) (i : PathIntermediateIndex C b σ P h) (D : Clause (Live σ)) (hD : pathReducedClause C b σ P h i = some D) : D.width ≤ b

theorem Complexity.DepthThreeLowerBound.path_fill_agree_outside_remainder {V : Type uDepth1} {I : Type uDepth2} [Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (x : Cube (Live σ)) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) (v : V) : v ∉ liveSet σ \ pathFinalSet C σ P → fill σ x v = fill σ (pathCenter C σ P) v

theorem Complexity.DepthThreeLowerBound.pathReducedClause_eval_on_support {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (x : Cube (Live σ)) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) (h : Fin P.length) (i : PathIntermediateIndex C b σ P h) : residualClauseEval (pathReducedClause C b σ P h i) x = (C ↑i).eval (fill σ x)

theorem Complexity.DepthThreeLowerBound.pathCoveredCount_eq_on_support {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (x : Cube (Live σ)) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) (h : Fin P.length) : coveredCount (fun (i : I) => (C i).scope) (liveSet σ) (fun (i : I) => (C i).violation (fill σ x)) (pathPrefixSet C σ P h) = pathCoveredCount C σ P h

theorem Complexity.DepthThreeLowerBound.pathMarkerBad_card {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (x : Cube (Live σ)) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) (h : Fin P.length) : (markerBad (fun (i : PathIntermediateIndex C b σ P h) (z : Cube (Live σ)) => residualClauseEval (pathReducedClause C b σ P h i) z) x).card = intermediateCount (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) (pathPrefixSet C σ P h)

theorem Complexity.DepthThreeLowerBound.path_easyCount_eq_marker_count {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (x : Cube (Live σ)) (hx : ∀ i ∈ P, (C i).violation (fill σ x) = true) (h : Fin P.length) : easyCount (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) (pathPrefixSet C σ P h) = pathCoveredCount C σ P h + (markerBad (fun (i : PathIntermediateIndex C b σ P h) (z : Cube (Live σ)) => residualClauseEval (pathReducedClause C b σ P h i) z) x).card

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.PathMarkerSample {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) : Type uDepth2

A collection of marker choices along a path.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.pathMixtureCNF {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (K : CNF (Live σ)) (π : PathMarkerSample C b σ P) : CNF (Live σ)

The CNF obtained from a path and its marker samples.

Equations

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

theorem Complexity.DepthThreeLowerBound.pathMixtureCNF_widthAtMost {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (P : List I) (K : CNF (Live σ)) (hb : 1 ≤ b) (hK : K.WidthAtMost b) (π : PathMarkerSample C b σ P) : (pathMixtureCNF C b σ P K π).WidthAtMost b

theorem Complexity.DepthThreeLowerBound.pathMixture_scaled_average {V : Type uDepth1} {I : Type uDepth2} [Fintype V] [Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) {n : ℕ} {P : List I} (hP : P ∈ paths (fun (i : I) => (C i).scope) (liveSet σ) b n) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) (K : CNF (Live σ)) (x : Cube (Live σ)) : (pathWeight C σ P * finiteAvg fun (π : PathMarkerSample C b σ P) => indicator ((pathMixtureCNF C b σ P K π).eval x)) = indicator (K.eval x) * if ∀ i ∈ P, (C i).violation (fill σ x) = true then ∏ h : Fin P.length, (↑(easyCount (fun (i : I) => (C i).scope) (liveSet σ) b (fun (i : I) => (C i).violation (fill σ x)) (pathPrefixSet C σ P h)))⁻¹ else 0