Top step of the flip-flop

For k = t ε_{m+1}^{β-γ}, t ≥ 1/2: log (KBar(k)/(√(9/80) ε_m^{β+γ})) equals log (t √(80/9)) up to O(ε_m^δ).

theorem AVenhance.Infra.FullTheorem.FlipFlop.top_step {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {t : ℝ} (ht : 1 / 2 ≤ t) (hr : 4 * epsilon β I.Λ m ^ delta β ≤ 1) (hsm : 2 * ksConst β * epsilon β I.Λ m ≤ 1) : |Real.log (I.KhomScalar (t * epsilon β I.Λ (m + 1) ^ (β - gamma β)) (m + 1) / (√(9 / 80) * epsilon β I.Λ m ^ (β + gamma β))) - Real.log (t * √(80 / 9))| ≤ (4 + 2 * (β - gamma β) * ksConst β) * epsilon β I.Λ m ^ delta β