Unrestricted depth-three lower bound: hard slice

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/HardSlice.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_language_slice_small_correlations (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∃ (α : Fin n → Fin (dataDimension n) ⊕ Bool), ∀ (H : CNF (Fin (dataDimension n))), H.WidthAtMost (degreeCutoff s (dataDimension n)) → |finiteAvg fun (x : Cube (Fin (dataDimension n))) => sign (language (List.ofFn (GateInput.assignment α x))) * indicator (H.eval x)| ≤ 6 * 2 ^ (-(64 * (s + 1) * √↑(dataDimension n)) / 16)