Fixed cutoff start above Q

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Range
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination

section
namespace D1Bound5






theorem _root_.D1Bound5.fixed_cutoff_start_above_Q (K S T C D : ℝ)
    (hK : 0 < K) (hS : 0 < S) (hT : 0 < T) (hC : 0 < C)
    (hgap : K*T^5/S^2 < C) (hstart : C^7/(S^2*T^4) < D)
    (hover : 1 < (1-1/4000 : ℝ)*K^4*T^10/(12100*S^10)) :
    4*55^2*T^6*C^3/(1-1/4000 : ℝ) < D := by sorry

end D1Bound5
end