The summable scalar budgets propagate the genuine low source guards and absorb the absolute geometric errors.

theorem EulerPacketInduction.Stage.initial_step_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (e : ℝ) (he : e ≤ EulerPacketInductionScales.initialIncrement S.J S.X n) : P.low.Be + e ≤ EulerBaseDatum.initialCoefficientCost + ∑ i ∈ Finset.range (n + 1), EulerPacketInductionScales.initialIncrement S.J S.X i ∧ P.low.Bc + e ≤ EulerPacketLowConstants.gradientConstant * S.X ^ 1000 + ∑ i ∈ Finset.range (n + 1), EulerPacketInductionScales.initialIncrement S.J S.X i

theorem EulerPacketInduction.Stage.pressure_step_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (e : ℝ) (he : e ≤ EulerPacketInductionScales.pressureIncrement S.J S.X n) : P.low.K + e ≤ EulerBaseDatum.initialCoefficientCost + EulerBaseDatum.literalInitialPressureCost S.D S.X + ∑ i ∈ Finset.range (n + 1), EulerPacketInductionScales.pressureIncrement S.J S.X i

theorem EulerPacketInduction.Stage.next_localized {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (T ei ep : ℝ) (hT : 0 ≤ T) (hTcap : T ≤ EulerPacketBaseGuardScales.baseHorizon S.J S.X) (hi0 : 0 ≤ ei) (hp0 : 0 ≤ ep) (hi : ei ≤ EulerPacketInductionScales.initialIncrement S.J S.X n) (hp : ep ≤ EulerPacketInductionScales.pressureIncrement S.J S.X n) : (P.low.K + ep) * (T ^ 2 / 2) + (P.low.Be + ei) * T + EulerMeanHarmonic.boundaryLocalizationC2 * (P.low.Bc + ei) * P.low.r ^ 3 * T ≤ 1 / 2

theorem EulerPacketInduction.Stage.ratio_absorption {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (r : ℝ) (hr : 0 ≤ r) (hbad : 2 * EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.shear S.J S.X n * r ≤ EulerPacketPressureScale.badCost S.J 4 EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant 80 (EulerPacketSourceScaleChoice.scaleSequence S.J S.X) n) : EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n + EulerPacketSourceScaleSequence.shear S.J S.X n * (EulerPacketGeometryLowBounds.goodRatio + r) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.shear S.J S.X n ∧ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n + 2 * EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.shear S.J S.X n * (EulerPacketGeometryLowBounds.goodRatio + r) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.shear S.J S.X n * EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInduction.Stage.next_frame_bounds {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} : 1 ≤ EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.previousShear S.J S.X n) ∧ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n ≤ EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.previousShear S.J S.X n) ∧ (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) ^ 2 + EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n ≤ (EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.previousShear S.J S.X n)) ^ 2

theorem EulerPacketInduction.Stage.coupling_step {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (a : ℝ) (h : |a / P.frame.a - 1| ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 c EulerPacketLowConstants.frameConstant S.X n) : |a - 1| ≤ 2 * ∑ i ∈ Finset.range (n + 1), EulerParentRenewalScale.renewalCost S.J S.D 4 c EulerPacketLowConstants.frameConstant S.X i

theorem EulerPacketInduction.Stage.tilt_step {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (σ : ℝ) (h : |EulerPacketSourceScaleChoice.scaleSequence S.J S.X (n + 1) ^ 2 * σ ^ 2 - 1| ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 c EulerPacketLowConstants.frameConstant S.X n) : 1 / 2 ≤ σ ^ 2 * EulerPacketSourceScaleChoice.scaleSequence S.J S.X (n + 1) ^ 2 ∧ σ ^ 2 * EulerPacketSourceScaleChoice.scaleSequence S.J S.X (n + 1) ^ 2 ≤ 2

theorem EulerParentPacketFrames.RenewalAtTarget.background_compression_of_error_le_one {ι V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (e : ℝ) (he : e ≤ 1) : inner ℝ ((P.B G.targetTime) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime))) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime)) + e < 0