Vanishing initial-time Gaussian error

The fourth-root spatial split and all-orders integral flatness make the weighted initial cutoff term vanish.

theorem ESS.uc_initial_time_error_tendsto_zero (ρ : ℝ) (hρ : 4 ≤ ρ) (a : ℝ) (ha : 0 ≤ a) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (ucCylinder ρ) MeasureTheory.volume) (hflat : UCIntegralFlatness 0 ρ 2 v) : Filter.Tendsto (fun (ε : ℝ) => ε ^ (-2) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Icc ε (2 * ε)), ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Integral flatness makes the weighted initial-time cutoff error vanish as the transition shrinks to time zero.