Unrestricted depth-three lower bound: restriction count split

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/RestrictionCountSplit.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.intermediateIndices {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (U : Finset V) : Finset I

Clauses classified as intermediate at the current revealed set.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_intermediateIndices {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (U : Finset V) (i : I) : i ∈ intermediateIndices scope T b U ↔ 0 < (residual scope T U i).card ∧ (residual scope T U i).card ≤ b

noncomputable def Complexity.DepthThreeLowerBound.intermediateCount {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (U : Finset V) : ℕ

The number of intermediate clauses satisfying the selection condition.

Equations

• Complexity.DepthThreeLowerBound.intermediateCount scope T b violation U = {i ∈ Complexity.DepthThreeLowerBound.intermediateIndices scope T b U | violation i = true}.card

theorem Complexity.DepthThreeLowerBound.easyCount_eq_covered_add_intermediate {V : Type uDepth1} {I : Type uDepth2} [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (U : Finset V) : easyCount scope T b violation U = coveredCount scope T violation U + intermediateCount scope T b violation U

theorem Complexity.DepthThreeLowerBound.subtype_filter_card {I : Type uDepth2} (s : Finset I) (p : I → Prop) [DecidablePred p] : {i : ↥s | p ↑i}.card = (Finset.filter p s).card