Support of a raw packet witness is exactly support of its actual L² path.

theorem EulerPacketCylinderField.Field.supported_of_raw_zero {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (h : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) : G.path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerPacketCylinderField.Field.raw_zero_of_supported {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsClosed S) (h : ∀ (t : ↑(Set.Icc 0 T)), G.path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : raw (↑t, x, θ) = 0