The actual mean solver closes a grade at its constant source profile. Only fixed source costs are absorbed into the radius; the grade amplitude cancels without any loss.

theorem EulerPacketCylinderField.Field.normalized_const_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (c : ℝ) (hc : 0 < c) : (G.normalized hT (ContinuousMap.const (↑(Set.Icc 0 T)) c) ⋯).path = (G.smul c⁻¹).path

theorem EulerPacketCylinderField.Field.WordBound.normalize_const {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) (c : ℝ) (hc : 0 < c) {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R (A * c) d) : (G.normalized hT (ContinuousMap.const (↑(Set.Icc 0 T)) c) ⋯).WordBound q R A d

theorem EulerPacketCylinderField.Field.WordBound.of_normalized_const {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) (c : ℝ) (hc : 0 < c) {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT (ContinuousMap.const (↑(Set.Icc 0 T)) c) ⋯).WordBound q R A d) : G.WordBound q R (c * A) d

structure EulerMeanPacketProvider.Budget.GradeGuards {D : Data} {R : ℝ} (L : Budget D 6 R) : Prop

The mean source costs are fixed before selecting any grade or its profile.

• velocity : L.velocityCost ≤ R
• derivative : L.derivativeCost ≤ R
• pressureGradient : L.pressureGradientCost ≤ R

theorem EulerMeanPacketProvider.Budget.grade_bounds {P : ℝ} [Fact (0 < P)] {D : Data} {R : ℝ} (L : Budget D 6 R) (W : L.GradeGuards) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T)) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (p : ℕ) (hp : 2 ≤ p) (hforce : (F.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanForceShift p)) : ((Forcing.vectorCylinderField P G).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p) ∧ ((Forcing.vectorDerivativeCylinderField P G).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p) ∧ ((G.pressureGradientCylinderField P).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)

The three actual mean outputs satisfy the unit budget at b_p=H₀^(2p−2) and the same external radius.

theorem EulerMeanPacketProvider.Budget.vector_grade_bound {P : ℝ} [Fact (0 < P)] {D : Data} {R : ℝ} (L : Budget D 6 R) (W : L.GradeGuards) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T)) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (p : ℕ) (hp : 2 ≤ p) (hforce : (F.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanForceShift p)) : ((Forcing.vectorCylinderField P G).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)

theorem EulerMeanPacketProvider.Budget.derivative_grade_bound {P : ℝ} [Fact (0 < P)] {D : Data} {R : ℝ} (L : Budget D 6 R) (W : L.GradeGuards) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T)) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (p : ℕ) (hp : 2 ≤ p) (hforce : (F.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanForceShift p)) : ((Forcing.vectorDerivativeCylinderField P G).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)

theorem EulerMeanPacketProvider.Budget.pressure_gradient_grade_bound {P : ℝ} [Fact (0 < P)] {D : Data} {R : ℝ} (L : Budget D 6 R) (W : L.GradeGuards) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T)) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (p : ℕ) (hp : 2 ≤ p) (hforce : (F.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanForceShift p)) : ((G.pressureGradientCylinderField P).normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)