The old-corrector time term and old pressure term use the same fixed coefficient budget.

theorem EulerPacketCylinderField.CoefficientBudget.slowCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : B.slowCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.fastCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : B.fastCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.linearCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : B.linearCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.multiplierCost_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : B.multiplierCost ≤ B.termCost

theorem EulerPacketCylinderField.CoefficientBudget.previousLinear_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) (hT : 0 < T) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)) (p : ℕ) (b : C(↑(Set.Icc 0 T), ℝ)) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (htime : TimeDerivative ⋯ G H) {R : ℝ} (hG : (G.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1))) (hH : (H.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1))) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) B.Rc ≤ R) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), (S.high (p - 1)) t ≤ b t) : ((Field.linearPart C.strain G H hT htime O.interval ⋯).normalized ⋯ b hb).WordBound 6 R B.linearCost (EulerPacketShiftArithmetic.highShift (p - 1))

theorem EulerPacketCylinderField.CoefficientBudget.previousPressure_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) (hT : 0 < T) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)) (p : ℕ) (b : C(↑(Set.Icc 0 T), ℝ)) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) (q : EulerPacketProfileRecursion.ScalarField) (G : Field P T (pressureGradient q)) {R : ℝ} (hG : (G.normalized ⋯ (S.high (p - 1)) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift (p - 1))) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) B.Rc ≤ R) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), (S.high (p - 1)) t ≤ b t) : ((Field.slowPressure C.inverse q G).normalized ⋯ b hb).WordBound 6 R B.multiplierCost (EulerPacketShiftArithmetic.highShift (p - 1))