The proved raw-field contract of the concrete admissible mean solver.

theorem EulerMeanPacketProvider.meanSolve_angle_independent (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (t : ℝ) (x : EulerSmoothLimit.Space) (θ η : ℝ) : (meanSolve D raw).1 (t, x, θ) = (meanSolve D raw).1 (t, x, η) ∧ (meanSolve D raw).2 (t, x, θ) = (meanSolve D raw).2 (t, x, η)

theorem EulerMeanPacketProvider.meanSolve_divergence (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => (D.inverseFrame (↑t, y, θ)) ((meanSolve D raw).1 (↑t, y, θ))) x = 0

theorem EulerMeanPacketProvider.meanSolve_initial_support (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (θ : ℝ) : (tsupport fun (x : EulerSmoothLimit.Space) => (meanSolve D raw).1 (0, x, θ)) ⊆ {x : EulerSmoothLimit.Space | ‖D.ℓ • x‖ ≤ 2}

theorem EulerMeanPacketProvider.meanSolve_initial_compact (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (θ : ℝ) : HasCompactSupport fun (x : EulerSmoothLimit.Space) => (meanSolve D raw).1 (0, x, θ)

theorem EulerMeanPacketProvider.meanSolve_joint_continuous (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) : Continuous fun (z : ↑(Set.Icc 0 D.T) × EulerSmoothLimit.Space × ℝ) => (meanSolve D raw).1 (↑z.1, z.2)

theorem EulerMeanPacketProvider.meanSolve_angle_jets (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (meanSolve D raw).1 (t, x, θ)).2 EulerPacketPointJets.angleDirection = 0 ∧ (EulerPacketPointJets.pressureJet (meanSolve D raw).2 (t, x, θ)).2 EulerPacketPointJets.angleDirection = 0