Choosing the short-time parabolic scale

The rescaling parameter is chosen from the fixed Carleman constant and the lower-order coefficient, while remaining below the Gaussian time threshold of lem:bu-gaussian.

theorem ESS.bu_short_scale_choice (c c₁ γ : ℝ) (hc : 0 < c) (hγ : 0 < γ) : ∃ (γ₁ : ℝ), 0 < γ₁ ∧ γ₁ ≤ γ / 2 ∧ 0 < √(2 * γ₁) ∧ √(2 * γ₁) ≤ 1 ∧ c * 36 * (c₁ * √(2 * γ₁)) ^ 2 ≤ 1 / 2

A positive Gaussian time threshold admits a smaller scale that absorbs the weak differential inequality uniformly over all cutoffs.