Gaussian suppression away from the flatness center

Outside the quarter-power spatial ball, the initial transition carries a Gaussian factor that dominates every inverse power of its time scale.

theorem ESS.ucGaussianWeight_le_far_initial {ε a r : ℝ} (hε : 0 < ε) (ha : 0 ≤ a) (hr : 0 < r) (hεsmall : ε ≤ 1) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hslo : ε ≤ z.2) (hshi : z.2 ≤ 2 * ε) (hfar : z.1 ∉ CKN.Foundation.Parabolic.vec3Ball 0 r) : ucGaussianWeight a z ≤ (ε * Real.exp (-(1 / 3))) ^ (-2 * a) * Real.exp (-(r ^ 2 / (8 * ε)))

During the initial transition, the Gaussian weight is exponentially small outside a spatial ball of radius r.