Lean rpow bookkeeping with a ℕ-parameter in the exponent (1/(2κ), 1 - 1/(5κ))

When exponents depend on a natural κ (e.g. q ≥ (c√N)^{1/κ} from q^κ ≥ c√N), these steps worked in Mathlib: Real.rpow_le_rpow then Real.pow_rpow_inv_natCast to undo (q^κ)^{κ⁻¹}; build √((c√n)^{κ⁻¹}) = c^{1/(2κ)} n^{1/(4κ)} with Real.sqrt_eq_rpow, ← Real.rpow_mul, Real.mul_rpow, then congr 2 and field_simp on each exponent goal (one goal also needs ring; with <;> ring the unusedTactic linter complains about the goal that does not need it). Real.log_le_rpow_div with ε = 1/(40κ) gives log y ≤ 40κ·y^ε after rw [div_div_eq_mul_div, div_one]. For exponent comparisons, prove facts like 1/(5κ) ≤ 1/5 once with div_le_div_iff₀ and finish with linarith. gcongr cannot discharge 0 ≤ 1 - 1/(5κ) (positivity fails on subtraction), so pass Real.rpow_le_rpow the side condition by hand. push_neg is deprecated; use push Not.