Unrestricted depth-three lower bound: hard slice eventual

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

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

theorem Complexity.DepthThreeLowerBound.exists_good_language_slice_eventually (b : ℕ) (hb : 1 ≤ b) (B : ℝ) (hB : 0 < B) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∃ (α : Fin n → Fin (dataDimension n) ⊕ Bool), (restrictionAvg (liveProbability B (dataDimension n)) fun (σ : Restriction (Fin (dataDimension n))) => if ¬goodRestriction (liveProbability B (dataDimension n)) (2 ^ (-(B * √↑(dataDimension n)) / 16)) b (fun (x : Cube (Fin (dataDimension n))) => language (List.ofFn (GateInput.assignment α x))) σ then 1 else 0) ≤ 4 * 2 ^ (-(B * √↑(dataDimension n)) / 16)