Geometry for moving a Gaussian center

A small neighborhood of a new center stays inside the source cylinder, and its covering centers satisfy the Gaussian output conditions.

theorem ESS.uc_move_center_geometry (x₀ y₀ : CKN.Foundation.Parabolic.Vec3) (R T γ : ℝ) (hR : 0 < R) (hT : 0 < T) (hγ : 0 < γ) (hy : y₀ ∈ CKN.Foundation.Parabolic.vec3Ball x₀ (ucRadiusFraction * R)) (hyneq : y₀ ≠ x₀) : ∃ (L : ℝ) (S : ℝ) (δ : ℝ), 0 < L ∧ 0 < S ∧ 0 < δ ∧ δ ≤ L / 4 ∧ δ ≤ √(S / 2) ∧ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball y₀ L) (Set.Ioo 0 S) ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T) ∧ ∀ (r : ℝ), 0 < r → r < δ → ∀ (n : ℕ), ∀ c ∈ CKN.Foundation.Parabolic.vec3Ball y₀ (2 * r), CKN.Foundation.Parabolic.vec3EuclideanNorm (c - x₀) ≤ ucRadiusFraction * R ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm (y₀ - x₀) / 2 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (c - x₀) ∧ 3 / 5 * (3 / 4) ^ n * r ^ 2 ≤ γ * T ∧ 16 / 100 * (3 / 5 * (3 / 4) ^ n * r ^ 2) ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (c - x₀) ^ 2

The geometric parameters for transferring Gaussian decay to a nearby spatial center.