Uniform, explicit frequency guards for the actual packet correction. A single polynomial source bound suffices simultaneously for all five requirements. No eventual threshold is hidden in this statement.
theorem
EulerPacketFiveCost.fiveEnvelope_components
(P : ℝ)
[Fact (0 < P)]
(X : ℝ)
(hX : 0 ≤ X)
:
EulerPacketCoarseMajorant.tailPolynomialConstant X X X ≤ fiveEnvelope P X ∧ X ≤ fiveEnvelope P X ∧ 12 * growthEnvelope P X * X ≤ fiveEnvelope P X ∧ 8 * growthEnvelope P X * X * EulerPacketCorrectionConstants.drift X X X * inverseRadiusEnvelope X ≤ fiveEnvelope P X ∧ 8 * growthEnvelope P X * X * inverseRadiusEnvelope X ≤ fiveEnvelope P X
theorem
EulerPacketFiveCost.five_costs_bound
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P)
(R H C CT X : ℝ)
(hX : 1 ≤ X)
(hR : 0 ≤ R)
(hH : 0 ≤ H)
(hC : 0 ≤ C)
(hRX : R ≤ X)
(hHX : H ≤ X)
(hCX : C ≤ X)
(hCTX : CT ≤ X)
(hi : D.inverseBound ≤ X)
(hm : EulerPacketCorrectionCoefficients.inverseMetricBound D ≤ X)
(hf : EulerPacketCorrectionCoefficients.inverseMetricFirstBound D ≤ X)
(ht : EulerPacketCorrectionCoefficients.inverseMetricTimeBound D ≤ X)
(hB : Kc.B ≤ X)
(hM : Kc.M ≤ X)
(hA0 : Kc.A0 ≤ X)
(hA2 : Kc.A2 ≤ X)
(hRc : Kc.Rc ≤ X)
(hT : D.T ≤ X)
:
EulerPacketCoarseMajorant.tailPolynomialConstant R H CT ≤ costConstant P * X ^ costPower P ∧ C ≤ costConstant P * X ^ costPower P ∧ 12 * EulerPacketCorrectionConstants.growth D P Kc R H C * D.T ≤ costConstant P * X ^ costPower P ∧ 8 * EulerPacketCorrectionConstants.growth D P Kc R H C * D.T * EulerPacketCorrectionConstants.drift R H C / EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc ≤ costConstant P * X ^ costPower P ∧ 8 * EulerPacketCorrectionConstants.growth D P Kc R H C * D.T / EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc ≤ costConstant P * X ^ costPower P
theorem
EulerPacketFiveCost.frequency_guards
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P)
(R H C CT X : ℝ)
(hX : 1 ≤ X)
(hR : 0 ≤ R)
(hH : 0 ≤ H)
(hC : 0 ≤ C)
(hRX : R ≤ X)
(hHX : H ≤ X)
(hCX : C ≤ X)
(hCTX : CT ≤ X)
(hi : D.inverseBound ≤ X)
(hm : EulerPacketCorrectionCoefficients.inverseMetricBound D ≤ X)
(hf : EulerPacketCorrectionCoefficients.inverseMetricFirstBound D ≤ X)
(ht : EulerPacketCorrectionCoefficients.inverseMetricTimeBound D ≤ X)
(hB : Kc.B ≤ X)
(hM : Kc.M ≤ X)
(hA0 : Kc.A0 ≤ X)
(hA2 : Kc.A2 ≤ X)
(hRc : Kc.Rc ≤ X)
(hT : D.T ≤ X)
(k : ℝ)
(hbudget : costConstant P * X ^ costPower P ≤ EulerPacketSourceFrequency.smallPower k)
:
EulerPacketCoarseMajorant.tailPolynomialConstant R H CT ≤ EulerPacketSourceFrequency.smallPower k ∧ C ≤ EulerPacketSourceFrequency.smallPower k ∧ 12 * EulerPacketCorrectionConstants.growth D P Kc R H C * D.T ≤ EulerPacketSourceFrequency.smallPower k ∧ 8 * EulerPacketCorrectionConstants.growth D P Kc R H C * D.T * EulerPacketCorrectionConstants.drift R H C / EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc ≤ EulerPacketSourceFrequency.smallPower k ∧ 8 * EulerPacketCorrectionConstants.growth D P Kc R H C * D.T / EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc ≤ EulerPacketSourceFrequency.smallPower k
The literal source frequency assumptions follow from one explicit polynomial comparison; the threshold does not depend on a chosen parent.