Exponentially small literal residual for the actual zero-history packet.

theorem EulerPacketCylinderField.forwardTailSum_normalized_bound (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hTime : M.T = D.T) (Y : EulerTransversePacketProvider.InitialData P D) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB 1) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : CoefficientBudget (sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime)) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (α : ℝ) (hα : 0 < α) (hgrowth : timeProfileChange S.growth hTime = α • L.g) (hprimaryBudget : ProfileBudget (forwardSourcePrimaryWitness P M D hTime Y) S L.R 1) (N : ℕ) (hN : 1 ≤ N) (k X : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) (hcoef : BC.multiplierCost ≤ k ^ (1 / 100)) (hX : 6 ≤ X) (hNX : X - 1 ≤ ↑N) : (((sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime).inverse.multiply (sourceTailSumField P M D hTime (EulerTransversePacketProvider.InitialData.zero P D) Y N k⁻¹)).smul k).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0

theorem EulerPacketCylinderField.forwardResidual_normalized_bound (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hTime : M.T = D.T) (Y : EulerTransversePacketProvider.InitialData P D) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB 1) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : CoefficientBudget (sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime)) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (α : ℝ) (hα : 0 < α) (hgrowth : timeProfileChange S.growth hTime = α • L.g) (hprimaryBudget : ProfileBudget (forwardSourcePrimaryWitness P M D hTime Y) S L.R 1) (Cagree : SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k X : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) (hcoef : BC.multiplierCost ≤ k ^ (1 / 100)) (hX : 6 ≤ X) (hNX : X - 1 ≤ ↑N) : (((sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime).inverse.multiply (sourceResidualField P M D hTime (EulerTransversePacketProvider.InitialData.zero P D) Y Cagree N hN k⁻¹ ⋯)).smul k).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0