The literal compact terminal wave initializes the mean-time packet budget.

theorem EulerPacketTerminalDatum.joinedTerminalPrimary_budget (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hTime : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (H : EulerTransversePacketPrimary.Budget L) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (hR : wordRadius (Fin 4) δ ≤ L.R) (W : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖)) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile) : EulerPacketCylinderField.ProfileBudget (EulerPacketCylinderField.joinedTerminalPrimaryWitness period M D hTime τ hτ hτT B (initialData D δ hδ (α • ξ) hs)) S L.R 1