Reusable upper certificates for arcsine potentials

theorem Zeta5Irrational.Uω_le_left_certificate {a b t s q U : ℝ} (hab : a < b) (ht : t ≤ a) (hs : 0 ≤ s) (hsq : (t - a) * (t - b) ≤ s ^ 2) (hq : ((a + b) / 2 - t + s) / 2 ≤ q) (hlog : Real.log q ≤ U) : Uω a b t ≤ U

An upper certificate for an arcsine potential to the left of its support.

theorem Zeta5Irrational.Uω_le_right_certificate {a b t s q U : ℝ} (hab : a < b) (ht : b ≤ t) (hs : 0 ≤ s) (hsq : (t - a) * (t - b) ≤ s ^ 2) (hq : (t - (a + b) / 2 + s) / 2 ≤ q) (hlog : Real.log q ≤ U) : Uω a b t ≤ U

An upper certificate for an arcsine potential to the right of its support.