Unrestricted depth-three lower bound: restriction expansion

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

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

def Complexity.DepthThreeLowerBound.violationValue {I : Type v} (violation : I → Bool) (i : I) : ℝ

The real indicator that a clause is violated.

Equations

• Complexity.DepthThreeLowerBound.violationValue violation i = if violation i = true then 1 else 0

def Complexity.DepthThreeLowerBound.totalCount {I : Type v} [instFintypeI : Fintype I] (violation : I → Bool) : ℕ

The total number of violated clauses in the indexed family.

Equations

• Complexity.DepthThreeLowerBound.totalCount violation = {i : I | violation i = true}.card

def Complexity.DepthThreeLowerBound.easyCount {V : Type u} {I : Type v} [DecidableEq V] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (U : Finset V) : ℕ

The number of violated clauses in the easy part of the family.

Equations

• Complexity.DepthThreeLowerBound.easyCount scope T b violation U = {i : I | (Complexity.DepthThreeLowerBound.residual scope T U i).card ≤ b ∧ violation i = true}.card

def Complexity.DepthThreeLowerBound.coveredCount {V : Type u} {I : Type v} [DecidableEq V] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (violation : I → Bool) (U : Finset V) : ℕ

The number of violated clauses covered by the revealed coordinates.

Equations

• Complexity.DepthThreeLowerBound.coveredCount scope T violation U = {i : I | Complexity.DepthThreeLowerBound.residual scope T U i = ∅ ∧ violation i = true}.card

def Complexity.DepthThreeLowerBound.pathNumerator {I : Type v} (violation : I → Bool) (P : List I) : ℝ

The product of violation indicators along a path.

Equations

• Complexity.DepthThreeLowerBound.pathNumerator violation P = (List.map (Complexity.DepthThreeLowerBound.violationValue violation) P).prod

def Complexity.DepthThreeLowerBound.pathDenominator {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) : ℝ

The product of covered-clause counts along a path.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.pathTerm {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) : ℝ

The numerator-to-denominator contribution of a path.

Equations

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

noncomputable def Complexity.DepthThreeLowerBound.pathResidual {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) : ℝ

The residual factor after the clauses on a path have been selected.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.pathNumerator_nil {I : Type v} (violation : I → Bool) : pathNumerator violation [] = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.pathNumerator_snoc {I : Type v} (violation : I → Bool) (P : List I) (i : I) : pathNumerator violation (P ++ [i]) = pathNumerator violation P * violationValue violation i

@[simp]

theorem Complexity.DepthThreeLowerBound.pathDenominator_nil {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) : pathDenominator scope T b violation [] = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.pathDenominator_snoc {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) (i : I) : pathDenominator scope T b violation (P ++ [i]) = pathDenominator scope T b violation P * ↑(easyCount scope T b violation (revealed scope T (P ++ [i])))

@[simp]

theorem Complexity.DepthThreeLowerBound.pathResidual_snoc {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) (i : I) : pathResidual scope T b violation (P ++ [i]) = pathNumerator violation (P ++ [i]) / (↑(totalCount violation) * pathDenominator scope T b violation P)

theorem Complexity.DepthThreeLowerBound.pathNumerator_ne_zero_iff {I : Type v} (violation : I → Bool) (P : List I) : pathNumerator violation P ≠ 0 ↔ ∀ i ∈ P, violation i = true

theorem Complexity.DepthThreeLowerBound.coveredCount_le_easyCount {V : Type u} {I : Type v} [DecidableEq V] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (U : Finset V) : coveredCount scope T violation U ≤ easyCount scope T b violation U

theorem Complexity.DepthThreeLowerBound.easyCount_le_totalCount {V : Type u} {I : Type v} [DecidableEq V] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (U : Finset V) : easyCount scope T b violation U ≤ totalCount violation

theorem Complexity.DepthThreeLowerBound.length_le_coveredCount_of_support {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) (hs : pathNumerator violation P ≠ 0) : P.length ≤ coveredCount scope T violation (revealed scope T P)

theorem Complexity.DepthThreeLowerBound.easyCount_pos_of_support {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b (n + 1)) (hs : pathNumerator violation P ≠ 0) : 0 < easyCount scope T b violation (revealed scope T P)

theorem Complexity.DepthThreeLowerBound.pathDenominator_pos_of_support {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b n) (hs : pathNumerator violation P ≠ 0) : 0 < pathDenominator scope T b violation P

theorem Complexity.DepthThreeLowerBound.totalCount_eq_easy_add_hard {V : Type u} {I : Type v} [DecidableEq V] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (U : Finset V) : ↑(totalCount violation) = ↑(easyCount scope T b violation U) + ∑ i ∈ hardIndices scope T b U, violationValue violation i

theorem Complexity.DepthThreeLowerBound.path_residual_identity {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b (n + 1)) (hq : totalCount violation ≠ 0) : pathResidual scope T b violation P = pathTerm scope T b violation P - ∑ i ∈ hardIndices scope T b (revealed scope T P), pathResidual scope T b violation (P ++ [i])

theorem Complexity.DepthThreeLowerBound.sum_path_residual_identity {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (n : ℕ) (hq : totalCount violation ≠ 0) : ∑ P ∈ paths scope T b (n + 1), pathResidual scope T b violation P = ∑ P ∈ paths scope T b (n + 1), pathTerm scope T b violation P - ∑ P ∈ paths scope T b (n + 2), pathResidual scope T b violation P

theorem Complexity.DepthThreeLowerBound.sum_initial_residual {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (he : easyCount scope T b violation ∅ = 0) (hq : totalCount violation ≠ 0) : ∑ P ∈ paths scope T b 1, pathResidual scope T b violation P = 1

theorem Complexity.DepthThreeLowerBound.finite_alternating_telescoping (t r : ℕ → ℝ) (h : ∀ (n : ℕ), r (n + 1) = t (n + 1) - r (n + 2)) (N : ℕ) : ∑ j ∈ Finset.range N, (-1) ^ (j + 1) * t (j + 1) = -r 1 + (-1) ^ N * r (N + 1)

theorem Complexity.DepthThreeLowerBound.pathTerm_zero_of_totalCount_zero {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) {n : ℕ} {P : List I} (hP : P ∈ paths scope T b (n + 1)) (hq : totalCount violation = 0) : pathTerm scope T b violation P = 0

theorem Complexity.DepthThreeLowerBound.finite_violation_expansion {V : Type u} {I : Type v} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) : (if totalCount violation = 0 then 1 else 0) = (if easyCount scope T b violation ∅ = 0 then 1 else 0) * (1 + ∑ j ∈ Finset.range (T.card / (b + 1)), (-1) ^ (j + 1) * ∑ P ∈ paths scope T b (j + 1), pathTerm scope T b violation P)