Lean: eliminating a free parameter m with Nat.ceil (logb 2 x) and rpow_logb

To turn a theorem with hypothesis 64 * β ≤ 2 ^ m into a parameter-free bound, set m := ⌈logb 2 (64 * β)⌉₊. Then 64 * β ≤ 2 ^ m follows from (Real.rpow_logb (by norm_num) (by norm_num) hpos).symm and Real.rpow_le_rpow_of_exponent_le one_le_two (Nat.le_ceil _) after rw [← Real.rpow_natCast]; m ≤ logb 2 (128 β) comes from Nat.ceil_lt_add_one + Real.logb_mul + Real.logb_self_eq_one. logb needs import Mathlib.Analysis.SpecialFunctions.Log.Base (not pulled in by Pow/Real). Real.log_two_lt_d9 was not available under that name; Real.log_lt_sub_one_of_pos (0 < 2) (2 ≠ 1) gives log 2 < 1, which is enough for log x ≤ logb 2 x when log x ≥ 0.