The raw forward field attains the actual continuous representative of its prescribed supported initial coordinates.

theorem EulerTransversePacketProvider.Forcing.vector_initial_of_representative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (f : EulerLiftedGradientSpace.LiftDomain P → U) (hf : Continuous f) (hrep : ↑↑↑I.value =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (y : EulerSmoothLimit.Space) (θ : ℝ) : G.vector I (0, y, θ) = ((D.frame.field ⟨0, ⋯⟩) y) (f (y, ↑θ))