Fixed source costs close the direct-forward packet grade bounds. The profile's positive scalar factor cancels exactly; one spare shift pays the fixed operator costs, with no change of external radius.

The genuine direct-forward solution has amplitude-linear estimates at one source-dependent radius, for arbitrary admissible initial data and forcing.

Homogeneity restores a common arbitrary envelope for genuine forcing and initial data, without adding either envelope to the radius guards.

theorem EulerTransversePacketProvider.pair_amplitude_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {ι : Type u_2} [Fintype ι] (S : {r : EulerPacketProfileRecursion.VectorField} → Forcing P D r → InitialData P D → C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hs : ∀ {r : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r) (I : InitialData P D), ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (S G I)) (hm : ∀ {r r' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r) (H : Forcing P D r') (I J : InitialData P D) (a : ℝ), H.path = a • G.path → J.value = a • I.value → S H J = a • S G I) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (R C : ℝ) (d e : ℕ) (hunit : ∀ {r : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r) (I : InitialData P D), (∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (HistoryData.forcingPath G))) n 0 ≤ EulerGevrey.majorant R d n) → (∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ EulerGevrey.majorant R d n) → ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (S G I))) n 0 ≤ C * EulerGevrey.majorant R e n) {r : EulerPacketProfileRecursion.VectorField} (G : Forcing P D r) (I : InitialData P D) (A : ℝ) (hA : 0 ≤ A) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant R d n) (hi : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (S G I))) n 0 ≤ C * A * EulerGevrey.majorant R e n

theorem EulerTransversePacketForward.Budget.velocity_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D ι q) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.fullVelocityPath I))) n 0 ≤ L.velocityCost * A * EulerGevrey.majorant L.R (d + 1) n

theorem EulerTransversePacketForward.Budget.derivative_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D ι q) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.fullDerivativePath I))) n 0 ≤ L.derivativeCost * A * EulerGevrey.majorant L.R (d + 1) n

theorem EulerTransversePacketForward.Budget.velocity_common_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D ι q) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.fullVelocityPath I))) n 0 ≤ L.commonCost * A * EulerGevrey.majorant L.R (d + 1) n

theorem EulerTransversePacketForward.Budget.derivative_common_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D ι q) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.fullDerivativePath I))) n 0 ≤ L.commonCost * A * EulerGevrey.majorant L.R (d + 1) n

All eight genuine direct-forward outputs obey one fixed mixed-word Sobolev budget. The input radius is retained, both data amplitudes remain outside the solve, and at most two derivative shifts are spent. All normalization uses the literal positive time profile without differentiating that profile.

Same-radius estimates for the actual corrector, divided by the prescribed time profile.

theorem EulerTransversePacketProvider.Forcing.potentialPath_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (q : ℕ) (Rc C R A : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (d : ℕ) (hbA : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.fullVelocityPath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (hbK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.potentialPath I))) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * (P * A) * EulerGevrey.majorant R d n

theorem EulerTransversePacketProvider.Forcing.potentialTimePath_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (q : ℕ) (Rc C R A : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (d : ℕ) (hbA : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.fullVelocityPath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (hbAt : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.fullDerivativePath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (hbK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hbKt : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.potentialTimePath I))) n 0 ≤ 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * (P * A) * EulerGevrey.majorant R d n

theorem EulerTransversePacketProvider.Forcing.correctorPath_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (q : ℕ) (Rc C R A : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (d : ℕ) (hbA : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.fullVelocityPath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (hbK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hbI : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.correctorPath I))) n 0 ≤ 27 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C ^ 2 * (P * A) * EulerGevrey.majorant R (d + 1) n

theorem EulerTransversePacketProvider.Forcing.correctorTimePath_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (q : ℕ) (Rc C R A : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (d : ℕ) (hbA : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.fullVelocityPath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (hbAt : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.fullDerivativePath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (hbK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hbKt : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hbI : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hbIt : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.correctorTimePath I))) n 0 ≤ 108 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C ^ 2 * (P * A) * EulerGevrey.majorant R (d + 1) n

Bounds for the actual high-pressure gradient from the normalized forcing and solved velocity.

theorem EulerTransversePacketProvider.Forcing.pressurePath_normalized_eq_source {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) : (EulerContinuousTimeWeight.normalize g hg) (G.pressurePath I) = EulerSourceNormalResidualBounds.sourcePressure P D.M D.normal D.normalLower ⋯ ⋯ ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) G.path)) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) (G.velocityPath I)))

theorem EulerTransversePacketProvider.Forcing.scalarGradientField_normalized_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (q : ℕ) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.pressurePath I))) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.scalarGradientField I).path)) n 0 ≤ 3 * A * EulerGevrey.majorant R (d + 1) n

theorem EulerTransversePacketProvider.Forcing.source_pressure_gradient_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (q : ℕ) (Rc Cm CM Ri R Af Av : ℝ) (hRc : 0 ≤ Rc) (hCm : 0 ≤ Cm) (hCM : 0 ≤ CM) (hAf : 0 ≤ Af) (hAv : 0 ≤ Av) (hRi : 2 * EulerTimeLpGramGevrey.gramCost D.normalLower Cm 1 * (Rc + 1) ≤ Ri) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (4 * Ri) ≤ R) (hm : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.normal.field t)) x‖ ≤ Cm * EulerGevrey.majorant Rc 0 n) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.M.field t)) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hf : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) G.path))) n 0 ≤ Af * EulerGevrey.majorant R d n) (hv : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath P D.support ⋯) (G.velocityPath I)))) n 0 ≤ Av * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (G.scalarGradientField I).path)) n 0 ≤ 3 * (P * EulerSourceNormalResidualBounds.pressureCost (Fin 4) q Ri Cm CM Af Av) * EulerGevrey.majorant R (d + 1) n

def EulerTransversePacketForward.Budget.pressureAmplitude {P : ℝ} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) : ℝ

Pressure amplitude, given by P*pressureCost (Fin 4) q N.Ri N.C N.C 1 L.commonCost.

Equations

• L.pressureAmplitude N = P * EulerSourceNormalResidualBounds.pressureCost (Fin 4) q N.Ri N.C N.C 1 L.commonCost

def EulerTransversePacketForward.Budget.potentialAmplitude {P : ℝ} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) : ℝ

Potential amplitude, given by 3*N.blockAmplitude*(P*L.commonCost).

Equations

• L.potentialAmplitude N = 3 * N.blockAmplitude * (P * L.commonCost)

def EulerTransversePacketForward.Budget.potentialTimeAmplitude {P : ℝ} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) : ℝ

Potential time amplitude, given by 6*N.blockAmplitude*(P*L.commonCost).

Equations

• L.potentialTimeAmplitude N = 6 * N.blockAmplitude * (P * L.commonCost)

def EulerTransversePacketForward.Budget.correctorAmplitude {P : ℝ} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) : ℝ

Corrector amplitude, given by 27*N.blockAmplitude^2*(P*L.commonCost).

Equations

• L.correctorAmplitude N = 27 * N.blockAmplitude ^ 2 * (P * L.commonCost)

def EulerTransversePacketForward.Budget.correctorTimeAmplitude {P : ℝ} {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) : ℝ

Corrector time amplitude, given by 108*N.blockAmplitude^2*(P*L.commonCost).

Equations

• L.correctorTimeAmplitude N = 108 * N.blockAmplitude ^ 2 * (P * L.commonCost)

theorem EulerTransversePacketForward.Budget.pressure_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.pressurePath I))) n 0 ≤ L.pressureAmplitude N * A * EulerGevrey.majorant L.R (d + 1) n

theorem EulerTransversePacketForward.Budget.pressure_gradient_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.scalarGradientField I).path)) n 0 ≤ 3 * L.pressureAmplitude N * A * EulerGevrey.majorant L.R (d + 2) n

theorem EulerTransversePacketForward.Budget.potential_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.potentialPath I))) n 0 ≤ L.potentialAmplitude N * A * EulerGevrey.majorant L.R (d + 1) n

theorem EulerTransversePacketForward.Budget.potential_time_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.potentialTimePath I))) n 0 ≤ L.potentialTimeAmplitude N * A * EulerGevrey.majorant L.R (d + 1) n

theorem EulerTransversePacketForward.Budget.corrector_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.correctorPath I))) n 0 ≤ L.correctorAmplitude N * A * EulerGevrey.majorant L.R (d + 2) n

theorem EulerTransversePacketForward.Budget.corrector_time_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} (L : Budget D (Fin 4) q) (N : EulerTransversePacketJoin.NormalBudget D q L.R) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (A : ℝ) (hA : 0 ≤ A) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ A * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ A * EulerGevrey.majorant L.R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (G.correctorTimePath I))) n 0 ≤ L.correctorTimeAmplitude N * A * EulerGevrey.majorant L.R (d + 2) n

theorem EulerTransversePacketForward.Budget.pressureAmplitude_nonneg {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) : 0 ≤ L.pressureAmplitude N

theorem EulerTransversePacketForward.Budget.correctorAmplitude_nonneg {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) : 0 ≤ L.correctorAmplitude N

theorem EulerTransversePacketForward.Budget.correctorTimeAmplitude_nonneg {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) : 0 ≤ L.correctorTimeAmplitude N

structure EulerTransversePacketForward.Budget.GradeGuards {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) (C : ℝ) : Prop

The unscaled data cost is fixed before the positive amplitude and grade. It is one for forced profiles and the literal compact-wave cost for the primary.

• data_nonneg : 0 ≤ C
• common : L.commonCost * C ≤ L.R
• corrector : L.correctorAmplitude N * C ≤ L.R
• correctorTime : L.correctorTimeAmplitude N * C ≤ L.R
• pressureGradient : 3 * L.pressureAmplitude N * C ≤ L.R

theorem EulerTransversePacketForward.Budget.grade_fields {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) (C : ℝ) (W : L.GradeGuards N C) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (c : ℝ) (hc : 0 < c) (d e : ℕ) (hroom : d + 3 ≤ e) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G))) n 0 ≤ c * C * EulerGevrey.majorant L.R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ c * C * EulerGevrey.majorant L.R d n) : ((G.vectorField I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e ∧ ((G.vectorDerivativeField I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e ∧ ((G.curlCorrectorField I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e ∧ ((G.correctorDerivativeField I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e ∧ ((G.scalarGradientField I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e