Unrestricted depth-three lower bound: restriction path data

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

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

def Complexity.DepthThreeLowerBound.pathCompatible {V : Type uDepth1} {I : Type uDepth2} (C : I → Clause V) (σ : Restriction V) (P : List I) : Prop

There is an extension of the restriction violating every clause on the path.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.pathCenter {V : Type uDepth1} {I : Type uDepth2} (C : I → Clause V) (σ : Restriction V) (P : List I) : Cube (Live σ)

Choose a witnessing assignment for a compatible path, or all false otherwise.

Equations

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

theorem Complexity.DepthThreeLowerBound.pathCenter_support {V : Type uDepth1} {I : Type uDepth2} (C : I → Clause V) (σ : Restriction V) (P : List I) (h : pathCompatible C σ P) (i : I) : i ∈ P → (C i).violation (fill σ (pathCenter C σ P)) = true

@[simp]

theorem Complexity.DepthThreeLowerBound.pathCompatible_nil {V : Type uDepth1} {I : Type uDepth2} (C : I → Clause V) (σ : Restriction V) : pathCompatible C σ []

noncomputable def Complexity.DepthThreeLowerBound.pathPrefixSet {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) (h : Fin P.length) : Finset V

Live variables revealed by a prefix of the clause path.

Equations

• Complexity.DepthThreeLowerBound.pathPrefixSet C σ P h = Complexity.DepthThreeLowerBound.revealed (fun (i : I) => (C i).scope) (Complexity.DepthThreeLowerBound.liveSet σ) (List.take (↑h + 1) P)

noncomputable def Complexity.DepthThreeLowerBound.pathFinalSet {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) : Finset V

Live variables revealed by the complete clause path.

Equations

• Complexity.DepthThreeLowerBound.pathFinalSet C σ P = Complexity.DepthThreeLowerBound.revealed (fun (i : I) => (C i).scope) (Complexity.DepthThreeLowerBound.liveSet σ) P

noncomputable def Complexity.DepthThreeLowerBound.pathLiveSet {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) : Finset (Live σ)

The revealed variables viewed as elements of the restriction's live set.

Equations

• Complexity.DepthThreeLowerBound.pathLiveSet C σ P = {v : Complexity.DepthThreeLowerBound.Live σ | ↑v ∈ Complexity.DepthThreeLowerBound.pathFinalSet C σ P}

noncomputable def Complexity.DepthThreeLowerBound.pathCoveredCount {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) (h : Fin P.length) : ℕ

The covered-clause count at a path prefix under its witnessing assignment.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.pathWeight {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) : ℝ

The product of reciprocal covered-clause counts along the path.

Equations

• Complexity.DepthThreeLowerBound.pathWeight C σ P = ∏ h : Fin P.length, (↑(Complexity.DepthThreeLowerBound.pathCoveredCount C σ P h))⁻¹

noncomputable def Complexity.DepthThreeLowerBound.pathCost {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (j : ℕ) : ℝ

Sum the weights of compatible paths of a fixed length.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.restrictionCost {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : ℝ

Sum the compatible-path costs over all allowed lengths.

Equations

• Complexity.DepthThreeLowerBound.restrictionCost C b σ = ∑ j ∈ Finset.range (Fintype.card V / (b + 1) + 1), Complexity.DepthThreeLowerBound.pathCost C b σ j

theorem Complexity.DepthThreeLowerBound.pathWeight_nonneg {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) : 0 ≤ pathWeight C σ P

theorem Complexity.DepthThreeLowerBound.pathCost_nonneg {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) (j : ℕ) : 0 ≤ pathCost C b σ j

theorem Complexity.DepthThreeLowerBound.restrictionCost_nonneg {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : 0 ≤ restrictionCost C b σ

@[simp]

theorem Complexity.DepthThreeLowerBound.pathWeight_nil {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (σ : Restriction V) : pathWeight C σ [] = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.pathCost_zero {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (b : ℕ) (σ : Restriction V) : pathCost C b σ 0 = 1

theorem Complexity.DepthThreeLowerBound.pathPrefixSet_subset_final {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) (h : Fin P.length) : pathPrefixSet C σ P h ⊆ pathFinalSet C σ P

theorem Complexity.DepthThreeLowerBound.pathCoveredCount_pos {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : 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) (hc : pathCompatible C σ P) (h : Fin P.length) : 0 < pathCoveredCount C σ P h

theorem Complexity.DepthThreeLowerBound.pathLiveSet_image {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) : Finset.image Subtype.val (pathLiveSet C σ P) = pathFinalSet C σ P

theorem Complexity.DepthThreeLowerBound.pathLiveSet_card {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] (C : I → Clause V) (σ : Restriction V) (P : List I) : (pathLiveSet C σ P).card = (pathFinalSet C σ P).card

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

theorem Complexity.DepthThreeLowerBound.path_cylinder_probability {V : Type uDepth1} {I : Type uDepth2} [instFintypeV : Fintype V] [instFintypeI : Fintype I] (C : I → Clause V) (σ : Restriction V) (P : List I) (hn : ∀ i ∈ P, (C i).Normalized) (hc : pathCompatible C σ P) : (finiteAvg fun (x : Cube (Live σ)) => indicator (decide (∀ i ∈ P, (C i).violation (fill σ x) = true))) = (2 ^ (pathFinalSet C σ P).card)⁻¹