Unrestricted depth-three lower bound: tape parameter cost

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

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

theorem Complexity.DepthThreeLowerBound.TapeParameterCost.power_cost {k : ℕ} (hk : k ≤ 6) (c : ℕ) : TapePower.cost k 1 c ≤ 108 * (c + 1) ^ 7

theorem Complexity.DepthThreeLowerBound.TapeParameterCost.compare_cost {k : ℕ} (hk : k ≤ 6) (c D : ℕ) : TapePowerCompare.cost k c D ≤ 124 * (c + 1) ^ 7

theorem Complexity.DepthThreeLowerBound.TapeParameterCost.body_cost {k : ℕ} (hk : k ≤ 6) (two : Bool) (c : ℕ) : TapeSearchBody.cost k two c ≤ 16 * (c + 1) ^ 7

theorem Complexity.DepthThreeLowerBound.TapeParameterCost.search_cost {k : ℕ} (hk : k ≤ 6) (two : Bool) (D fuel c B : ℕ) (hc : c + TapeSearchBody.amount two * fuel ≤ B) : TapePowerSearch.cost k two D fuel c ≤ (fuel + 1) * 144 * (B + 1) ^ 7

theorem Complexity.DepthThreeLowerBound.TapeParameterCost.cube_cost (d : ℕ) : TapeParameterSearch.cubeCost d ≤ 200 * (d + 3) ^ 8

theorem Complexity.DepthThreeLowerBound.TapeParameterCost.sixth_cost (d : ℕ) : TapeParameterSearch.sixthCost d ≤ 200 * (d + 3) ^ 8