The complete constructed transverse path satisfies the literal packet equation on the whole closed interval.

theorem EulerTransversePacketJoin.scalar_smooth {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => scalar τ hτ hτT B G (t, y)

theorem EulerTransversePacketJoin.equation {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vectorDerivative τ hτ hτT B G (↑t, x, θ) + (D.strain (↑t, x, θ)) (vector τ hτ hτT B G (↑t, x, θ)) + deriv (fun (s : ℝ) => scalar τ hτ hτT B G (↑t, x, s)) θ • D.normalField (↑t, x, θ) = raw (↑t, x, θ)

The complete actual high field and normalized pressure satisfy (11), including at the history/forward junction.

theorem EulerTransversePacketJoin.jet_equation {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (vector τ hτ hτT B G) (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet (scalar τ hτ hτT B G) (↑t, x, θ)) = raw (↑t, x, θ)

The literal sliced-jet equation consumed by the packet grade recursion.