Small scale for the Gaussian estimate

A positive time fraction absorbs the normalized lower order term.

theorem ESS.uc_gaussian_small_scale (c₀ c₁ : ℝ) (hc₀ : 0 < c₀) (hc₁ : 0 < c₁) : ∃ (γ : ℝ), 0 < γ ∧ γ < 3 / 16 ∧ ∀ (T t scale : ℝ), 0 < T → T ≤ 1 → 0 < t → t ≤ γ * T → scale ^ 2 = 2 * t → c₀ * 54 * (c₁ * scale) ^ 2 ≤ 1 / 40

One time fraction works for all output points in the Gaussian estimate.