The literal polynomial first-packet scales satisfy every local, frequency and localized lower-bound guard after the final base choice.

The manuscript's literal first-packet scales have a fixed monomial frequency cost. The exponent and coefficient do not depend on J or X.

theorem EulerBaseDatum.firstParameterSize_literal (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) : firstParameterSize (EulerPacketBaseGuardScales.baseHorizon J X) (X ^ (-1010)) (X ^ 1000) ≤ (7 + solutionLabelConstant) * X ^ 1010

noncomputable def EulerBaseDatum.firstFrequencyConstant : ℝ

First frequency constant, given by frequencyConstant*(7+solutionLabelConstant)^frequencyPower.

Equations

• EulerBaseDatum.firstFrequencyConstant = EulerPacketUniformSource.frequencyConstant * (7 + EulerBaseDatum.solutionLabelConstant) ^ EulerPacketUniformSource.frequencyPower

noncomputable def EulerBaseDatum.firstFrequencyPower : ℕ

First frequency power, given by 1010*frequencyPower.

Equations

• EulerBaseDatum.firstFrequencyPower = 1010 * EulerPacketUniformSource.frequencyPower

theorem EulerBaseDatum.firstFrequencyConstant_pos : 0 < firstFrequencyConstant

theorem EulerBaseDatum.first_frequency_cost_bound (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) : EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope (firstParameterSize (EulerPacketBaseGuardScales.baseHorizon J X) (X ^ (-1010)) (X ^ 1000)) ^ EulerPacketInitializedOutputCost.uniformPower ≤ firstFrequencyConstant * X ^ firstFrequencyPower

theorem EulerBaseDatum.first_frequency_guard_eventually (J : ℕ) (hJ : 1 ≤ J) (D : ℕ) (hD : ↑firstFrequencyPower < ↑D * (EulerPacketSourceFrequency.theta / 100)) : ∀ᶠ (X : ℝ) in Filter.atTop, EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope (firstParameterSize (EulerPacketBaseGuardScales.baseHorizon J X) (X ^ (-1010)) (X ^ 1000)) ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower (X ^ D)

This remaining threshold depends only on the fixed base exponent, not on a parent or on a stage of the subsequent induction.

noncomputable def EulerBaseDatum.literalInitialError (D : ℕ) (X : ℝ) : ℝ

Literal initial error, given by (X^D)^(-(1/4 : ℝ)).

Equations

• EulerBaseDatum.literalInitialError D X = (X ^ D) ^ (-(1 / 4))

noncomputable def EulerBaseDatum.literalInitialPressureCost (D : ℕ) (X : ℝ) : ℝ

Literal initial pressure cost, given by 2*initialCoefficientCost*X^(-1010 : ℝ)*(X^1000*firstRatio)+literalInitialError D X.

Equations

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

theorem EulerBaseDatum.literalInitialError_nonneg (D : ℕ) (X : ℝ) (hX : 0 ≤ X) : 0 ≤ literalInitialError D X

theorem EulerBaseDatum.literalInitialError_tendsto_zero (D : ℕ) (hD : 0 < D) : Filter.Tendsto (literalInitialError D) Filter.atTop (nhds 0)

theorem EulerBaseDatum.literalInitialPressureCost_tendsto_zero (D : ℕ) (hD : 0 < D) : Filter.Tendsto (literalInitialPressureCost D) Filter.atTop (nhds 0)

theorem EulerBaseDatum.literal_radius_frequency_bound (D : ℕ) (hD : 2000 ≤ D) (X : ℝ) (hX : 1 ≤ X) : (EulerPacketBaseGuardScales.baseRadius X)⁻¹ ≤ (X ^ D) ^ (3 / 4)

structure EulerBaseDatum.FirstScaleGuards (J D : ℕ) (X : ℝ) : Prop

First scale guards data, collecting x_one, radius_small, local_time, frequency, label_frequency, radius_frequency and their compatibility conditions.

• x_one : 1 ≤ X
• radius_small : EulerPacketBaseGuardScales.baseRadius X ≤ 1 / 4
• local_time : EulerPacketBaseGuardScales.baseHorizon J X ≤ initialTime
• frequency : EulerPacketSourceFrequency.UniversalFrequency (X ^ D)
• label_frequency : solutionLabelConstant ≤ X ^ D
• radius_frequency : (EulerPacketBaseGuardScales.baseRadius X)⁻¹ ≤ (X ^ D) ^ (3 / 4)
• source_frequency : EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope (firstParameterSize (EulerPacketBaseGuardScales.baseHorizon J X) (X ^ (-1010)) (X ^ 1000)) ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower (X ^ D)
• error_small : literalInitialError D X ≤ 1
• pressure_small : literalInitialPressureCost D X ≤ 1 / 4
• localized : (initialCoefficientCost + literalInitialPressureCost D X) * (EulerPacketBaseGuardScales.baseHorizon J X ^ 2 / 2) + initialCoefficientCost * EulerPacketBaseGuardScales.baseHorizon J X + EulerMeanHarmonic.boundaryLocalizationC2 * (initialCoefficientCost + X ^ 1000 * EulerPacketFirstLowBounds.firstRatio + literalInitialError D X) * EulerPacketBaseGuardScales.baseRadius X ^ 3 * EulerPacketBaseGuardScales.baseHorizon J X ≤ 1 / 2

theorem EulerBaseDatum.eventually_firstScaleGuards (J : ℕ) (hJ : 1 ≤ J) (D : ℕ) (hD : 2000 ≤ D) (hDfreq : ↑firstFrequencyPower < ↑D * (EulerPacketSourceFrequency.theta / 100)) : ∀ᶠ (X : ℝ) in Filter.atTop, FirstScaleGuards J D X