A raw cylinder field determines its actual continuous L² path uniquely.

theorem EulerPacketCylinderField.Field.path_eq_of_same_raw {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G H : Field P T raw) : G.path = H.path

theorem EulerPacketCylinderField.Field.path_eq_of_raw_eq {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = raw (↑t, x, θ)) : G.path = H.path