The direct-forward source radius and its literal common-radius enlargement obey the same fixed polynomial envelope as the joined branch. The homogeneous growth constant is arbitrary and remains an input.

theorem EulerPacketForwardRadius.source_radius_le (T R C C1 Cp W : ℝ) (hW : 1 ≤ W) (hT0 : 0 ≤ T) (hT1 : T ≤ 1) (hR0 : 0 ≤ R) (hR : R ≤ W) (hC0 : 0 ≤ C) (hC : C ≤ W) (hC10 : 0 ≤ C1) (hC1 : C1 ≤ W) (hCp0 : 0 ≤ Cp) (hCp : Cp ≤ W) (hRi : EulerPacketParentTransverseCosts.inverseRadius R C ≤ W) : EulerPacketParentForwardBudget.radius 6 T R C C1 Cp ≤ EulerPacketSourceRadius.sourceRadiusEnvelope W

theorem EulerPacketForwardRadius.inverse_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) : 0 ≤ L.Ri

theorem EulerPacketForwardRadius.common_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (W : ℝ) (hW : 0 ≤ W) (hR : L.Rc ≤ W) (hC : L.C₀ ≤ W) (hC1 : L.C₁ ≤ W) (hI : L.Ri ≤ W) : L.commonCost ≤ EulerPacketRadiusPolynomial.commonEnvelope W

theorem EulerPacketForwardRadius.grade_sum_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : ℝ) (hW : 0 ≤ W) (hNR : N.Rc ≤ W) (hNC : N.C ≤ W) (hNI : N.Ri ≤ W) (hcommon : L.commonCost ≤ EulerPacketRadiusPolynomial.commonEnvelope W) : L.commonCost + L.correctorAmplitude N + L.correctorTimeAmplitude N + 3 * L.pressureAmplitude N ≤ EulerPacketRadiusPolynomial.gradeEnvelope W

noncomputable def EulerPacketForwardRadius.canonicalRadius {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (δ : ℝ) (ξ : U) : ℝ

Canonical radius, given by EulerPacketForwardCommonRadius.commonRadius LM L N BC (wordCost (Fin 4) 6 δ*‖ξ‖) (wordRadius (Fin 4) δ).

Equations

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

structure EulerPacketForwardRadius.RadiusPrimitives {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (δ : ℝ) (ξ : U) (W : ℝ) : Prop

Radius primitives data, collecting one, total_time, mean_time, mean_inverse_time, original_forward, original_mean and their compatibility conditions.

• one : 1 ≤ W
• total_time : D.T ≤ 1
• mean_time : M.T ≤ 1
• mean_inverse_time : M.T⁻¹ ≤ W
• original_forward : L.R ≤ W
• original_mean : Rm ≤ W
• forward_radius : L.Rc ≤ W
• forward_frame : L.C₀ ≤ W
• forward_first : L.C₁ ≤ W
• forward_inverse : L.Ri ≤ W
• normal_radius : N.Rc ≤ W
• normal_amplitude : N.C ≤ W
• normal_inverse : N.Ri ≤ W
• mean_radius : LM.Rc ≤ W
• mean_frame : LM.CF ≤ W
• mean_first : LM.CF₁ ≤ W
• mean_forcing : LM.Cf ≤ W
• coefficient_radius : BC.Rc ≤ W
• coefficient_cost : BC.termCost ≤ W
• delta_inverse : δ⁻¹ ≤ W
• terminal : ‖ξ‖ ≤ W

theorem EulerPacketForwardRadius.canonicalRadius_le_envelope {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (δ : ℝ) (ξ : U) (W : ℝ) (hδ : 0 < δ) (H : RadiusPrimitives L LM N BC δ ξ W) : canonicalRadius L LM N BC δ ξ ≤ EulerPacketRadiusPolynomial.radiusEnvelope W

theorem EulerPacketForwardRadius.canonicalRadius_power {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : EulerTransversePacketForward.Budget D (Fin 4) 6) {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (N : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (δ : ℝ) (ξ : U) (W : ℝ) (hδ : 0 < δ) (H : RadiusPrimitives L LM N BC δ ξ W) : canonicalRadius L LM N BC δ ξ ≤ EulerPacketRadiusPolynomial.radiusConstant * W ^ EulerPacketRadiusPolynomial.radiusPower