The actual joined and forward source budgets retain the polynomial correction envelope. Only their original coefficient leaves enter it.

theorem EulerTransversePacketJoin.Budget.correctionCoefficients_primitive_bound {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τ ⋯)} (L : Budget D τ hτ hτT B (Fin 4) 6) (NB : NormalBudget D 6 L.R) (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) (hLR : L.Rc ≤ X) (hNR : NB.Rc ≤ X) (hC0 : L.C₀ ≤ X) (hC1 : L.C₁ ≤ X) (hCI : NB.C ≤ X) : EulerPacketCorrectionPrimitive.CorrectionBounds D P (L.correctionCoefficients NB P) (EulerPacketCorrectionPrimitive.primitiveEnvelope P X)

theorem EulerTransversePacketJoin.Budget.correctionCoefficients_primitive_power {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τ ⋯)} (L : Budget D τ hτ hτT B (Fin 4) 6) (NB : NormalBudget D 6 L.R) (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) (hLR : L.Rc ≤ X) (hNR : NB.Rc ≤ X) (hC0 : L.C₀ ≤ X) (hC1 : L.C₁ ≤ X) (hCI : NB.C ≤ X) : EulerPacketCorrectionPrimitive.CorrectionBounds D P (L.correctionCoefficients NB P) (EulerPacketCorrectionPrimitive.primitiveConstant P * X ^ EulerPacketCorrectionPrimitive.primitivePower P)

theorem EulerTransversePacketForward.Budget.correctionCoefficients_primitive_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) (hLR : L.Rc ≤ X) (hNR : NB.Rc ≤ X) (hC0 : L.C₀ ≤ X) (hC1 : L.C₁ ≤ X) (hCI : NB.C ≤ X) : EulerPacketCorrectionPrimitive.CorrectionBounds D P (L.correctionCoefficients NB P) (EulerPacketCorrectionPrimitive.primitiveEnvelope P X)

theorem EulerTransversePacketForward.Budget.correctionCoefficients_primitive_power {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) (hLR : L.Rc ≤ X) (hNR : NB.Rc ≤ X) (hC0 : L.C₀ ≤ X) (hC1 : L.C₁ ≤ X) (hCI : NB.C ≤ X) : EulerPacketCorrectionPrimitive.CorrectionBounds D P (L.correctionCoefficients NB P) (EulerPacketCorrectionPrimitive.primitiveConstant P * X ^ EulerPacketCorrectionPrimitive.primitivePower P)