Literal joint parity is equivalent to parity of an actual cylinder-path witness.

theorem EulerPacketCylinderField.Field.reflection_eq_of_raw_parity {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (c : ℝ) (t : ↑(Set.Icc 0 T)) (h : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = c • raw (↑t, x, θ)) : (EulerCylinderFieldReflection.reflection P) (G.path t) = c • G.path t

theorem EulerPacketCylinderField.Field.raw_parity_of_reflection {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (c : ℝ) (t : ↑(Set.Icc 0 T)) (h : (EulerCylinderFieldReflection.reflection P) (G.path t) = c • G.path t) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, -x, -θ) = c • raw (↑t, x, θ)

theorem EulerPacketCylinderField.Field.reflection_neg_of_raw_odd {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (h : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) : (EulerCylinderFieldReflection.reflection P) (G.path t) = -G.path t

theorem EulerPacketCylinderField.Field.raw_odd_of_reflection_neg {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (h : (EulerCylinderFieldReflection.reflection P) (G.path t) = -G.path t) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, -x, -θ) = -raw (↑t, x, θ)