The constructed raw forward field has the prescribed actual initial data.

theorem EulerCylinderSmoothOrbit.pointField_zero_of_value_zero (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) (ht : p t = 0) (x : EulerLiftedGradientSpace.LiftDomain P) : pointField P p hp t x = 0

theorem EulerTransversePacketProvider.Forcing.coordinatePath_initial {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) : (G.coordinatePath I) ⟨0, ⋯⟩ = I.value

theorem EulerTransversePacketProvider.Forcing.velocityPath_initial {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) : (G.velocityPath I) ⟨0, ⋯⟩ = ((EulerLpCylinderRectangular.supportedOperatorMap P D.support ⋯) (D.frame.field ⟨0, ⋯⟩)) I.value

theorem EulerTransversePacketProvider.Forcing.vector_initial_of_zero {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) (hi : I.value = 0) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vector I (0, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.vector_zero_initial {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) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vector (InitialData.zero P D) (0, x, θ) = 0

theorem EulerTransversePacketProvider.highSolve_zero_initial {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : Data U) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing P D raw)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (highSolve P D (InitialData.zero P D) raw).1 (0, x, θ) = 0