Unrestricted depth-three lower bound: restriction path products

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

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

theorem Complexity.DepthThreeLowerBound.pathDenominator_eq_prod_prefix {V : Type u} {I : Type v} [DecidableEq V] [DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) : pathDenominator scope T b violation P = ∏ h : Fin P.length, ↑(easyCount scope T b violation (revealed scope T (List.take (↑h + 1) P)))

theorem Complexity.DepthThreeLowerBound.pathNumerator_eq_indicator_support {I : Type v} [DecidableEq I] [Fintype I] (violation : I → Bool) (P : List I) : pathNumerator violation P = if ∀ i ∈ P, violation i = true then 1 else 0

theorem Complexity.DepthThreeLowerBound.pathTerm_eq_support_prod_inv {V : Type u} {I : Type v} [DecidableEq V] [DecidableEq I] [Fintype I] (scope : I → Finset V) (T : Finset V) (b : ℕ) (violation : I → Bool) (P : List I) : pathTerm scope T b violation P = if ∀ i ∈ P, violation i = true then ∏ h : Fin P.length, (↑(easyCount scope T b violation (revealed scope T (List.take (↑h + 1) P))))⁻¹ else 0