Unrestricted depth-three lower bound: language search tests

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

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

theorem Complexity.DepthThreeLowerBound.cube_lt_iff_lt_hashDimension (d r : ℕ) : r ^ 3 < d ^ 2 ↔ r < hashDimension d

theorem Complexity.DepthThreeLowerBound.next_sixth_le_iff_lt_independenceOrder (d k : ℕ) (hk : Even k) : (k + 2) ^ 6 ≤ d ↔ k < independenceOrder d

theorem Complexity.DepthThreeLowerBound.cube_search_candidate_le_data {d r : ℕ} (h : r ≤ hashDimension d) : r ≤ d

theorem Complexity.DepthThreeLowerBound.sixth_search_candidate_le_data {d k : ℕ} (h : k ≤ independenceOrder d) : k ≤ d