Actual cylinder-path witnesses for raw packet fields

These records contain a genuine continuous L² path, its true smooth mixed translation orbit, and equality with the raw field on the time interval. Time derivatives are an actual L² evolution identity, stated separately.

structure EulerPacketCylinderField.Field (P T : ℝ) [Fact (0 < P)] (raw : EulerPacketProfileRecursion.VectorField) : Type

Field data, collecting path, orbit, raw_eq.

• path : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

  Time-dependent path of Field, of type C(Icc (0 : ℝ) T,LiftL2 P).

• orbit : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) self.path
• raw_eq (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, x, θ) = EulerCylinderSmoothOrbit.pointField P self.path ⋯ t (x, ↑θ)

def EulerPacketCylinderField.TimeDerivative {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (hT : 0 ≤ T) (G : Field P T raw) (H : Field P T raw_t) : Prop

The derivative witness is an actual within-interval derivative in the Hilbert L² space.

Equations

• EulerPacketCylinderField.TimeDerivative hT G H = ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT G.path) (H.path t) (Set.Icc 0 T) ↑t

theorem EulerPacketCylinderField.Field.raw_smooth {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)

theorem EulerPacketCylinderField.Field.raw_fderiv {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)) (x, θ) = EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P G.path ⋯ t) (x, ↑θ)

theorem EulerPacketCylinderField.Field.slicedJet_spatial {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (s : Set ℝ) (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet s raw (↑t, x, θ)).2 (EulerPacketPointJets.spatialInjection v) = (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P G.path ⋯ t) (x, ↑θ)) (v, 0)

theorem EulerPacketCylinderField.Field.slicedJet_angular {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (s : Set ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet s raw (↑t, x, θ)).2 EulerPacketPointJets.angleDirection = (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P G.path ⋯ t) (x, ↑θ)) (0, 1)

theorem EulerPacketCylinderField.Field.raw_hasDerivWithinAt {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (H : Field P T raw_t) (h : TimeDerivative hT G H) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivWithinAt (fun (r : ℝ) => raw (r, x, θ)) (raw_t (↑t, x, θ)) (Set.Icc 0 T) ↑t

theorem EulerPacketCylinderField.Field.slicedJet_temporal {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 < T) (H : Field P T raw_t) (h : TimeDerivative ⋯ G H) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet (Set.Icc 0 T) raw (↑t, x, θ)).2 EulerPacketPointJets.timeDirection = raw_t (↑t, x, θ)