Initial trace at the flatness center

The first pointwise vanishing order and continuity fix the trace at the origin.

theorem ESS.uc_origin_trace_zero (R T : ℝ) (hR : 0 < R) (hT : 0 < T) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ico 0 T))) (hvanish : ∀ (k : ℕ), ∃ (C : ℝ), ∀ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ C * (CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 + √z.2) ^ k) : w (0, 0) = 0

Pointwise first-order vanishing on the open cylinder forces a zero continuous initial trace at its center.