The time-zero amplification stage preserves the actual sharp physical derivative and upper pressure bounds. The early interval keeps its exponential gain, and the good interval retains the extra delta in the upper pressure estimate.

theorem EulerPacketPhysicalLowBounds.forwardPressureTerm_eq_coefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (ξ : U) (a slope : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : pressureTerm a slope ((D.M.field t) x) ((D.normal.field t) x) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) x) = (EulerPacketForwardShear.pressureCoefficient D ξ a t x * slope) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) x)) ((D.normal.field t) x)

def EulerParentPacketFrames.Evolution.ForwardSourceErrors {A : Parent} (E : Evolution A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k : ℝ) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (ev ep : ℝ) : Prop

The exact source (20) errors, expressed on the same normalized packet that defines the physical child. These are precisely the two errors supplied by the same-Q packet choice.

Equations

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

theorem EulerParentPacketFrames.Evolution.forwardSourceErrors_of_global {A : Parent} (E : Evolution A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k : ℝ) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (ev ep : ℝ) (herr : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k E.inverse t) x - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (E.inverse.normalized t x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (E.inverse.normalized t x))) (((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))‖ < ev ∧ ‖fderiv ℝ (gradient (A.normalizedPacketPressure m hm J support hSupport B residual k E.inverse t)) x - (EulerPacketForwardShear.pressureCoefficient (A.transverseData m hm J support hSupport) G.initialCoordinate (G.primaryAmplitude hball) t (E.inverse.normalized t x) * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (E.inverse.normalized t x))) • ((InnerProductSpace.rankOne ℝ) (((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))) (((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))‖ < ep) : E.ForwardSourceErrors m hm J support hSupport B residual k G hball ev ep

The literal strict errors returned by the global same-Q packet theorem imply the error record without any additional analytic bound.

theorem EulerParentPacketFrames.Evolution.exactForwardPacket_good_low_bounds {A : Parent} (E : Evolution A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep CM CH Kupper : ℝ) (herr : E.ForwardSourceErrors m hm J support hSupport B residual k G hball ev ep) (t : ↑(Set.Icc 0 A.T)) (ht : 1 ≤ EulerPacketMovingFrame.scaledTime 0 F.a F.epsilon ↑t) (x : EulerSmoothLimit.Space) (hCM : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM) (hCH : ‖fderiv ℝ (E.force t) x‖ ≤ CH) (hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y)) x‖ ≤ CM + G.hchild * EulerPacketGeometryLowBounds.goodRatio + ev ∧ ‖fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x‖ ≤ CH + 2 * CM * (G.hchild * EulerPacketGeometryLowBounds.goodRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x) z) z ≤ (Kupper + 2 * CM * G.δ * (G.hchild * EulerPacketGeometryLowBounds.goodRatio) + ep) * ‖z‖ ^ 2

theorem EulerParentPacketFrames.Evolution.exactForwardPacket_early_low_bounds {A : Parent} (E : Evolution A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep CM CH Kupper : ℝ) (herr : E.ForwardSourceErrors m hm J support hSupport B residual k G hball ev ep) (t : ↑(Set.Icc 0 A.T)) (ht : EulerPacketMovingFrame.scaledTime 0 F.a F.epsilon ↑t ≤ 1) (x : EulerSmoothLimit.Space) (hCM : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM) (hCH : ‖fderiv ℝ (E.force t) x‖ ≤ CH) (hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y)) x‖ ≤ CM + G.hchild * G.earlyRatio + ev ∧ ‖fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x‖ ≤ CH + 2 * CM * (G.hchild * G.earlyRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x) z) z ≤ (Kupper + 2 * CM * (G.hchild * G.earlyRatio) + ep) * ‖z‖ ^ 2

theorem EulerParentPacketFrames.Evolution.exactForwardPacket_whole_horizon_low_bounds {A : Parent} (E : Evolution A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep CM CH Kupper : ℝ) (herr : E.ForwardSourceErrors m hm J support hSupport B residual k G hball ev ep) (hCM : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (E.force t) x‖ ≤ CH) (hupper : ∀ (t : ↑(Set.Icc 0 A.T)) (x z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y)) x‖ ≤ CM + G.hchild * (EulerPacketGeometryLowBounds.goodRatio + G.earlyRatio) + ev ∧ ‖fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x‖ ≤ CH + 2 * CM * G.hchild * (EulerPacketGeometryLowBounds.goodRatio + G.earlyRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x) z) z ≤ (Kupper + 2 * CM * G.hchild * (G.δ * EulerPacketGeometryLowBounds.goodRatio + G.earlyRatio) + ep) * ‖z‖ ^ 2

The full horizon has one fixed absolute-size cost, while the upper pressure cost retains delta on good times and the exponentially small bad-time ratio. The parent constants remain the actual sharp CM and CH.