Unrestricted depth-three lower bound: hard slice parameters

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

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

theorem Complexity.DepthThreeLowerBound.sparseMomentBound_at_quarter (m b L h : ℕ) : sparseMomentBound m b L h (2 ^ (-↑m / 4)) = ↑(Fintype.card (SparseTestCode (Fin m) b L)) * ↑(2 * h) ^ (2 * h) * 2 ^ (-(↑m * ↑(2 * h)) / 4)

theorem Complexity.DepthThreeLowerBound.sparseMomentBound_quarter_le (m b M h : ℕ) (hm : 0 < m) (hh : 0 < h) (hcond : ↑M * (1 + ↑b * (Real.log (2 * ↑m + 1) / Real.log 2)) / ↑(2 * h) + Real.log ↑(2 * h) / Real.log 2 / ↑m ≤ 1 / 8) : sparseMomentBound m b (M * m) h (2 ^ (-↑m / 4)) ≤ 2 ^ (-(↑m * ↑(2 * h)) / 8)

theorem Complexity.DepthThreeLowerBound.exists_hashDimension_dominates (B : ℝ) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ (d : ℕ), D ≤ d → 33 / 16 * (B * √↑d) ≤ ↑(hashDimension d)

theorem Complexity.DepthThreeLowerBound.hard_slice_error_bound_eventually (b M : ℕ) (B : ℝ) (hB : 0 < B) : ∃ (D : ℕ), 4096 ≤ D ∧ ∀ (d : ℕ), D ≤ d → ∀ (m h : ℕ), B * √↑d / 2 ≤ ↑m → ↑m ≤ 2 * (B * √↑d) → 2 * h = independenceOrder d → 2 ^ (↑m - ↑(hashDimension d)) + sparseMomentBound m b (M * m) h (2 ^ (-↑m / 4)) ≤ 2 * 2 ^ (-(B * √↑d) / 16)

theorem Complexity.DepthThreeLowerBound.hash_collision_ratio_eq (m r : ℕ) : 2 ^ m / 2 ^ r = 2 ^ (↑m - ↑r)

theorem Complexity.DepthThreeLowerBound.actual_hard_slice_error_bound_eventually (b : ℕ) (hb : 1 ≤ b) (B : ℝ) (hB : 0 < B) : ∃ (D : ℕ), 4096 ≤ D ∧ ∀ (d : ℕ), D ≤ d → ∀ (m h : ℕ), B * √↑d / 2 ≤ ↑m → ↑m ≤ 2 * (B * √↑d) → 2 * h = independenceOrder d → 2 ^ m / 2 ^ hashDimension d + sparseMomentBound m b (hardSliceSparseConstant b hb * m) h (2 ^ (-↑m / 4)) ≤ 2 * 2 ^ (-(B * √↑d) / 16)