Unrestricted depth-three lower bound: restriction paths

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

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

def Complexity.DepthThreeLowerBound.revealed {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) : Finset V

The variables revealed by the selected sequence of clause scopes.

Equations

• Complexity.DepthThreeLowerBound.revealed scope T P = P.toFinset.biUnion fun (i : I) => scope i ∩ T

def Complexity.DepthThreeLowerBound.residual {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] (scope : I → Finset V) (T U : Finset V) (i : I) : Finset V

Coordinates remaining after the currently revealed set is removed.

Equations

• Complexity.DepthThreeLowerBound.residual scope T U i = scope i ∩ (T \ U)

@[simp]

theorem Complexity.DepthThreeLowerBound.revealed_nil {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) : revealed scope T [] = ∅

theorem Complexity.DepthThreeLowerBound.mem_revealed {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (v : V) : v ∈ revealed scope T P ↔ ∃ i ∈ P, v ∈ scope i ∧ v ∈ T

theorem Complexity.DepthThreeLowerBound.revealed_subset {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) : revealed scope T P ⊆ T

theorem Complexity.DepthThreeLowerBound.revealed_mono {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) {P Q : List I} (h : P ⊆ Q) : revealed scope T P ⊆ revealed scope T Q

@[simp]

theorem Complexity.DepthThreeLowerBound.revealed_snoc {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (i : I) : revealed scope T (P ++ [i]) = revealed scope T P ∪ scope i ∩ T

theorem Complexity.DepthThreeLowerBound.residual_eq_sdiff {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] (scope : I → Finset V) (T U : Finset V) (i : I) : residual scope T U i = (scope i ∩ T) \ U

theorem Complexity.DepthThreeLowerBound.residual_eq_empty_of_mem {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] {scope : I → Finset V} {T : Finset V} {P : List I} {i : I} (hi : i ∈ P) : residual scope T (revealed scope T P) i = ∅

theorem Complexity.DepthThreeLowerBound.card_revealed_snoc {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (i : I) : (revealed scope T (P ++ [i])).card = (revealed scope T P).card + (residual scope T (revealed scope T P) i).card

def Complexity.DepthThreeLowerBound.hardIndices {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (U : Finset V) : Finset I

Clause indices whose residual scope exceeds the width cutoff.

Equations

• Complexity.DepthThreeLowerBound.hardIndices scope T b U = {i : I | b < (Complexity.DepthThreeLowerBound.residual scope T U i).card}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_hardIndices {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (U : Finset V) (i : I) : i ∈ hardIndices scope T b U ↔ b < (residual scope T U i).card

def Complexity.DepthThreeLowerBound.paths {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) : ℕ → Finset (List I)

Admissible clause-index paths of the specified length.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.paths scope T b 0 = {[]}

@[simp]

theorem Complexity.DepthThreeLowerBound.paths_zero {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) : paths scope T b 0 = {[]}

theorem Complexity.DepthThreeLowerBound.paths_succ {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b n : ℕ) : paths scope T b (n + 1) = (paths scope T b n).biUnion fun (P : List I) => Finset.image (fun (i : I) => P ++ [i]) (hardIndices scope T b (revealed scope T P))

theorem Complexity.DepthThreeLowerBound.mem_paths_zero {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (P : List I) : P ∈ paths scope T b 0 ↔ P = []

theorem Complexity.DepthThreeLowerBound.mem_paths_succ {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] {scope : I → Finset V} {T : Finset V} {b n : ℕ} {P : List I} : P ∈ paths scope T b (n + 1) ↔ ∃ Q ∈ paths scope T b n, ∃ i ∈ hardIndices scope T b (revealed scope T Q), Q ++ [i] = P

theorem Complexity.DepthThreeLowerBound.snoc_mem_paths {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) {n : ℕ} {P : List I} {i : I} (hP : P ∈ paths scope T b n) (hi : i ∈ hardIndices scope T b (revealed scope T P)) : P ++ [i] ∈ paths scope T b (n + 1)

theorem Complexity.DepthThreeLowerBound.mem_paths_snoc_iff {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b n : ℕ) (P : List I) (i : I) : P ++ [i] ∈ paths scope T b (n + 1) ↔ P ∈ paths scope T b n ∧ i ∈ hardIndices scope T b (revealed scope T P)

theorem Complexity.DepthThreeLowerBound.length_of_mem_paths {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] {scope : I → Finset V} {T : Finset V} {b n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) : P.length = n

theorem Complexity.DepthThreeLowerBound.take_mem_paths {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) {k : ℕ} (hk : k ≤ n) : List.take k P ∈ paths scope T b k

theorem Complexity.DepthThreeLowerBound.not_mem_of_hard {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) {P : List I} {i : I} (hi : i ∈ hardIndices scope T b (revealed scope T P)) : i ∉ P

theorem Complexity.DepthThreeLowerBound.nodup_of_mem_paths {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] {scope : I → Finset V} {T : Finset V} {b n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) : P.Nodup

theorem Complexity.DepthThreeLowerBound.mul_le_revealed_card {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) : n * (b + 1) ≤ (revealed scope T P).card

theorem Complexity.DepthThreeLowerBound.length_mul_le_revealed_card {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) : P.length * (b + 1) ≤ (revealed scope T P).card

theorem Complexity.DepthThreeLowerBound.paths_eq_empty_of_card_lt {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b n : ℕ) (hn : T.card < n * (b + 1)) : paths scope T b n = ∅

theorem Complexity.DepthThreeLowerBound.paths_horizon_eq_empty {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) : paths scope T b (T.card / (b + 1) + 1) = ∅

theorem Complexity.DepthThreeLowerBound.sum_paths_succ {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b n : ℕ) {M : Type uDepth3} [AddCommMonoid M] (f : List I → M) : ∑ P ∈ paths scope T b (n + 1), f P = ∑ P ∈ paths scope T b n, ∑ i ∈ hardIndices scope T b (revealed scope T P), f (P ++ [i])