Genuine time-derivative witnesses are unique, including at both endpoints.

theorem EulerPacketCylinderField.TimeDerivative.raw_eq {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {raw raw₁ raw₂ : EulerPacketProfileRecursion.VectorField} {G H : Field P T raw} {G₁ : Field P T raw₁} {H₁ : Field P T raw₂} (hG : TimeDerivative ⋯ G G₁) (hH : TimeDerivative ⋯ H H₁) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw₁ (↑t, x, θ) = raw₂ (↑t, x, θ)

theorem EulerPacketCylinderField.TimeDerivative.path_eq {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {raw raw₁ raw₂ : EulerPacketProfileRecursion.VectorField} {G H : Field P T raw} {G₁ : Field P T raw₁} {H₁ : Field P T raw₂} (hG : TimeDerivative ⋯ G G₁) (hH : TimeDerivative ⋯ H H₁) : G₁.path = H₁.path