A single scale choice for the first packet and every normal stage. The record contains only numerical inequalities and convergent series; it does not assume the existence of a packet or of a future frame.

Reconstruct the numerical source guards from a supplied common finite cost budget, without making a second choice of the starting stage.

theorem EulerPacketSourceScaleChoice.uniformBounds_of_costs (J : ℕ) (hJ : 3 ≤ J) (C c δ : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (hδ : 0 ≤ δ) (A : ℕ) (x : ℕ → ℝ) (hx1 : ∀ (n : ℕ), 1 ≤ x n) (hsmall : ∀ (i : SourceCost), SmallSeries ((sourceCostSpec C c hC A i).cost J x) (δ / 3)) : UniformBounds J C c A x δ

theorem EulerPacketSourceScaleChoice.actualBounds_of_uniform (J D : ℕ) (hJ : 3 ≤ J) (C c X δ : ℝ) (hC : 1 ≤ C) (hc : 0 ≤ c) (hX : 1 ≤ X) (hδ : 0 ≤ δ) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (hbase : EulerPacketSourceScaleActual.baseErrorCost J D C X ≤ δ / 2) (hn : UniformBounds J C c 60 (scaleSequence J X) (δ / 32)) : EulerPacketSourceScaleActual.ActualBounds J D C c X δ

One starting index and one final base scale suffice for the actual geometric guards, pressure series, and any finite list of further packet frequency comparisons. No independently chosen index is substituted.

theorem EulerPacketCommonScaleChoice.exists_common_guards {ι : Type u_1} [Finite ι] (s : ι → EulerPacketSourceScaleChoice.CostSpec) (D : ℕ) (hD : 1000 ≤ D) (C c K CM CMn CHn cP : ℝ) (hC : 4 ≤ C) (hc : 0 ≤ c) (hK : 1 ≤ K) (hCM : 0 ≤ CM) (hCMn : 0 ≤ CMn) (hCHn : 0 ≤ CHn) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (η : ℝ), 0 < η → ∃ (X₀ : ℝ) (δ : ℝ), 8 ≤ X₀ ∧ 0 < δ ∧ δ ≤ η ∧ δ ≤ 1 / 2 ∧ ∀ (X : ℝ), X₀ ≤ X → EulerPacketSourceScaleActual.ActualBounds J D C c X δ ∧ (∀ (i : ι), EulerPacketSourceScaleChoice.SmallSeries ((s i).cost J (EulerPacketSourceScaleChoice.scaleSequence J X)) δ) ∧ EulerPacketSourceScaleChoice.SmallSeries (EulerPacketPressureScale.badCost J C CM CMn CHn cP (EulerPacketSourceScaleChoice.scaleSequence J X)) δ ∧ EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J (EulerPacketSourceScaleChoice.scaleSequence J X) n) δ ∧ ∀ (a β : ℕ → ℝ), (∀ (n : ℕ), 1 / 2 ≤ a n) → (∀ (n : ℕ), a n ≤ 2) → (∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) → (∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) → ∀ (n : ℕ), EulerPacketSourceScaleGuards.StageGuards J D C c X K a β n

noncomputable def EulerPacketInductionScales.geometryConstant : ℝ

Geometry constant, given by neighborStabilityConstant*frameConstant^2.

Equations

• EulerPacketInductionScales.geometryConstant = EulerPacketMovingFrame.neighborStabilityConstant * EulerPacketLowConstants.frameConstant ^ 2

theorem EulerPacketInductionScales.geometryConstant_one : 1 ≤ geometryConstant

noncomputable def EulerPacketInductionScales.activationMargin : ℝ

Activation margin, given by 1/(32*(activationConstant gradientConstant hessianConstant+1)).

Equations

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

theorem EulerPacketInductionScales.activationMargin_pos : 0 < activationMargin

theorem EulerPacketInductionScales.activationMargin_small : 16 * (EulerTransverseActivationSelection.activationConstant EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant + 1) * activationMargin ≤ 1

noncomputable def EulerPacketInductionScales.correctionCostSpec : EulerPacketSourceScaleChoice.CostSpec

Correction cost spec, bundling d, B, N, a and the required compatibility proofs.

Equations

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

theorem EulerPacketInductionScales.correctionCost_eq (J : ℕ) (X : ℝ) (n : ℕ) : correctionCostSpec.cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n = EulerPacketSourceScaleSequence.frequency J X n ^ (-(1 / 4))

noncomputable def EulerPacketInductionScales.extraCost : Unit ⊕ Bool → EulerPacketSourceScaleChoice.CostSpec

Extra cost used in packet induction scales.

Equations

• EulerPacketInductionScales.extraCost (Sum.inl val) = EulerNormalPacketParameters.frequencySpec 4
• EulerPacketInductionScales.extraCost (Sum.inr false) = EulerParentRenewalScale.activationCostSpec EulerPacketLowConstants.frameConstant EulerPacketInductionScales.extraCost._proof_1
• EulerPacketInductionScales.extraCost (Sum.inr true) = EulerPacketInductionScales.correctionCostSpec

noncomputable def EulerPacketInductionScales.initialIncrement (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Initial increment, given by badCost J 4 gradientConstant gradientConstant hessianConstant 80 (scaleSequence J X) n + (frequency J X n)^(-(1/4 : ℝ)).

Equations

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

noncomputable def EulerPacketInductionScales.pressureIncrement (J : ℕ) (X : ℝ) (n : ℕ) : ℝ

Pressure increment, given by `2gradientConstantEulerPacketGeometryLowBounds.goodRatio*goodCost J (scaleSequence J X) n

• initialIncrement J X n`.

Equations

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

structure EulerPacketInductionScales.Scales (c B : ℝ) : Type

Scales data, collecting J, D, X, δ, stage_large, base_power and their compatibility conditions.

• J : ℕ

  J of Scales, of type ℕ.

• D : ℕ

  Domain data of Scales, of type ℕ.

• X : ℝ

  X of Scales, of type ℝ.

• δ : ℝ

  Δ of Scales, of type ℝ.

• stage_large : 3 ≤ self.J
• base_power : 2000 ≤ self.D
• x_large : 8 ≤ self.X
• delta_pos : 0 < self.δ
• delta_small : self.δ ≤ 1 / 16
• delta_activation : self.δ ≤ activationMargin
• delta_geometry : 1000000 * geometryConstant * self.δ ≤ 1
• actual : EulerPacketSourceScaleActual.ActualBounds self.J self.D 4 c self.X self.δ
• first : EulerBaseDatum.FirstScaleGuards self.J self.D self.X
• normal_frequency (n : ℕ) : EulerPacketSourceFrequency.UniversalFrequency (EulerPacketSourceScaleSequence.frequency self.J self.X n)
• previous_floor (n : ℕ) : B ≤ EulerPacketSourceScaleSequence.previousFrequency self.J self.D self.X n
• frequency_series : EulerPacketSourceScaleChoice.SmallSeries ((EulerNormalPacketParameters.frequencySpec 4).cost self.J (EulerPacketSourceScaleChoice.scaleSequence self.J self.X)) self.δ
• activation_series : EulerPacketSourceScaleChoice.SmallSeries ((EulerParentRenewalScale.activationCostSpec EulerPacketLowConstants.frameConstant ⋯).cost self.J (EulerPacketSourceScaleChoice.scaleSequence self.J self.X)) self.δ
• correction_series : EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => EulerPacketSourceScaleSequence.frequency self.J self.X n ^ (-(1 / 4))) self.δ
• bad_series : EulerPacketSourceScaleChoice.SmallSeries (EulerPacketPressureScale.badCost self.J 4 EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant 80 (EulerPacketSourceScaleChoice.scaleSequence self.J self.X)) self.δ
• good_series : EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => 2 * EulerPacketLowConstants.gradientConstant * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost self.J (EulerPacketSourceScaleChoice.scaleSequence self.J self.X) n) self.δ
• renewal_series : EulerPacketSourceScaleChoice.SmallSeries (EulerParentRenewalScale.renewalCost self.J self.D 4 c EulerPacketLowConstants.frameConstant self.X) (1 / 4)
• time_small : EulerPacketBaseGuardScales.baseHorizon self.J self.X ≤ 1
• localized : EulerPacketBaseGuardScales.baseGuardCost self.J (EulerBaseDatum.initialCoefficientCost + 1) (EulerBaseDatum.initialCoefficientCost + 1) EulerPacketLowConstants.gradientConstant EulerMeanHarmonic.boundaryLocalizationC2 self.X ≤ 1 / 2

theorem EulerPacketInductionScales.exists_base_power : ∃ (D : ℕ), 2000 ≤ D ∧ ↑EulerBaseDatum.firstFrequencyPower < ↑D * (EulerPacketSourceFrequency.theta / 100)

theorem EulerPacketInductionScales.exists_scales (c B : ℝ) (hc : 0 ≤ c) : Nonempty (Scales c B)

theorem EulerPacketInductionScales.Scales.initial_series {c B : ℝ} (S : Scales c B) : EulerPacketSourceScaleChoice.SmallSeries (initialIncrement S.J S.X) (2 * S.δ)

theorem EulerPacketInductionScales.Scales.pressure_series {c B : ℝ} (S : Scales c B) : EulerPacketSourceScaleChoice.SmallSeries (pressureIncrement S.J S.X) (3 * S.δ)

theorem EulerPacketInductionScales.Scales.stage {c B : ℝ} (S : Scales c B) (a β : ℕ → ℝ) (n : ℕ) (ha : 1 / 2 ≤ a n) (ha2 : a n ≤ 2) (hβ : 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence S.J S.X n ^ 2) (hβ2 : β n * EulerPacketSourceScaleChoice.scaleSequence S.J S.X n ^ 2 ≤ 2) : EulerPacketSourceScaleGuards.StageGuards S.J S.D 4 c S.X geometryConstant a β n