Combining center Gaussian exponents

The small growth exponent and fixed normal phase are absorbed by the Gaussian average, leaving tangential lattice decay and a normal dyadic tail.

theorem ESS.bu_short_center_gaussian_absorption (G b β d : ℝ) (Y : CKN.Foundation.Parabolic.Vec3) (hGtan : G ≤ 1 / 16) (hGnorm : G ≤ β / 48) (hbβ : b ≤ β / 48) (hβ : 0 < β) (hd : 0 < d) (hd1 : d ≤ 1 / 2) (hY : 2 ≤ Y 2) : Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8) * Real.exp (b * Y 2 ^ 2) * Real.exp (G * (Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2)) * Real.exp (-(β * Y 2 ^ 2 / (12 * d))) ≤ Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 16) * Real.exp (-(β / (12 * d))) * Real.exp (-(β * Y 2 ^ 2 / (48 * d)))

The cell-center weights retain a tangential Gaussian, a normal Gaussian, and one dyadic normal tail (lem:bu-small-time).