Genuine within-time derivatives inherit the raw field's joint parity, including at the endpoints.

theorem EulerPacketCylinderField.Field.timeDerivative_parity {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hT : 0 < T) (hd : TimeDerivative ⋯ G H) (c : ℝ) (hpar : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = c • raw (↑t, x, θ)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw_t (↑t, -x, -θ) = c • raw_t (↑t, x, θ)

theorem EulerPacketCylinderField.Field.timeDerivative_odd {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hT : 0 < T) (hd : TimeDerivative ⋯ G H) (hpar : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw_t (↑t, -x, -θ) = -raw_t (↑t, x, θ)