The concrete mean inverse in the literal jets used by the packet recursion.

theorem EulerMeanPacketProvider.pressureJet_spatial_derivative (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (t, y)) (x, θ)) : (EulerPacketPointJets.pressureJet p (t, x, θ)).2 ∘SL EulerPacketPointJets.spatialInjection = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => p (t, y, θ)) x

The pressure jet is the ordinary spatial derivative at fixed time and angle.

theorem EulerMeanPacketProvider.slowPressure_pressureJet (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (t, y)) (x, θ)) : (EulerPacketPointJets.slowPressure FInv) (EulerPacketPointJets.pressureJet p (t, x, θ)) = (ContinuousLinearMap.adjoint FInv) (gradient (fun (y : EulerSmoothLimit.Space) => p (t, y, θ)) x)

theorem EulerMeanPacketProvider.Forcing.slicedJet_time {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) G.vector (↑t, x, θ)).2 EulerPacketPointJets.timeDirection = G.vectorDerivative (↑t, x, θ)

theorem EulerMeanPacketProvider.Forcing.jet_equation {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) G.vector (↑t, x, θ)) + (EulerPacketPointJets.slowPressure (D.inverseFrame (↑t, x, θ))) (EulerPacketPointJets.pressureJet G.scalar (↑t, x, θ)) = raw (↑t, x, θ)

This is exactly the pointwise mean equation required by the grade recursion.

theorem EulerMeanPacketProvider.Forcing.vector_angle_jet {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) G.vector (t, x, θ)).2 EulerPacketPointJets.angleDirection = 0

theorem EulerMeanPacketProvider.Forcing.scalar_angle_jet {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.pressureJet G.scalar (t, x, θ)).2 EulerPacketPointJets.angleDirection = 0

theorem EulerMeanPacketProvider.meanSolve_jet_equation (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (meanSolve D raw).1 (↑t, x, θ)) + (EulerPacketPointJets.slowPressure (D.inverseFrame (↑t, x, θ))) (EulerPacketPointJets.pressureJet (meanSolve D raw).2 (↑t, x, θ)) = raw (↑t, x, θ)

The total operator discharges the literal packet mean-jet interface on admissible inputs.