The algebraic conversion from the hard-instance query gap to the lower-bound complexity rate.

theorem V7.Stage5AboveTwoLowerS5F.rate_power_implication {p T A K eps : ℝ} (hp : 2 < p) (hT : 0 < T) (hA : 0 < A) (hK : 0 < K) (heps : 0 < eps) (hpower : T < (A / (K * eps)) ^ (p / (p + 2))) : eps < A / (K * T ^ (1 + 2 / p))