One fixed radius bounds every grade generated by the actual mean and zero-initial direct-forward solvers. Only the genuine primary datum remains as input; no later forcing or solution estimate is assumed.

One complete quantitative recursion step, using the actual mean and zero-initial direct-forward transverse solvers.

Every forced direct-forward grade starts from zero and obeys the genuine five-field grade budget at the common radius.

theorem EulerTransversePacketForward.Budget.forced_grade_bounds {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : Budget D (Fin 4) 6) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards N 1) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (F : EulerPacketCylinderField.Field P D.T raw) (c : ℝ) (hc : 0 < c) (p : ℕ) (hp : 2 ≤ p) (hforce : (F.normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p)) : ((G.vectorField (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p) ∧ ((G.vectorDerivativeField (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p) ∧ ((G.curlCorrectorField (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p) ∧ ((G.correctorDerivativeField (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p) ∧ ((G.scalarGradientField (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.forwardStep {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) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards N 1) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) {O : EulerPacketProfileRecursion.Operators} (C : CoefficientData P M.T O) (BC : CoefficientBudget C) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) (hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D (EulerTransversePacketProvider.InitialData.zero P D)) (hcorrector : O.curlCorrector = D.curlCorrector P) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (hp : 2 ≤ p) (G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i)) (hG : ∀ (i : ℕ) (hi : i < p), 1 ≤ i → ProfileBudget (G i hi) S L.R i) (hc₀ : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (c : ℝ) (hc : 0 < c) (hprofile : timeProfileChange (S.high p) hTime = c • L.g) (H : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.step O p a)) : ProfileBudget H S L.R p

noncomputable def EulerPacketCylinderField.forwardSourcePrimaryWitness (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) : ProfileRegularity P M.T ⋯ D.support (homogeneousPrimary D Y (sourceOperators P M D (EulerTransversePacketProvider.InitialData.zero P D)))

Forward source primary witness, given by (homogeneousPrimaryRegularity D Y (sourceOperators P M D (InitialData.zero P D)) rfl).changeTime hTime.symm M.T_pos.le.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketCylinderField.forwardSource_profile_budgets (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) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards N 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) (p : ℕ) : 1 ≤ p → ProfileBudget (sourceProfileWitness P M D hTime (EulerTransversePacketProvider.InitialData.zero P D) Y p) S L.R p