Unit pair height upper from orders

import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_OrdinaryLog10_Definitions

section
namespace D1Bound5






theorem _root_.D1Bound5.unit_pair_height_upper_from_orders (S D Z : ℝ)
    (hS : 10000 ≤ S) (hD : 0 < D) (hZ : 1 ≤ Z) (hprod : S*D < 2*Z^2)
    (horders : ∀ k : ℕ, 1 ≤ k →
      1 < 3*S*(42*S)^k/Z+Z/(2*(27*(S-1)^2/64)^k)) :
    ordinaryLog10 D < 7*ordinaryLog10 S+617/25+
      (118401/2500)/(ordinaryLog10 S-203/100) := by sorry



end D1Bound5
end