Numerical guard consequences for the literal scale sequences.

Packet Scale Activation

theorem EulerPacketScaleActivation.source_activation_ode_guards {j x β : ℝ} (hj : 3 ≤ j) (hx : 8 ≤ x) (hβx : 1 / 2 ≤ β * x ^ 2) (hβx₂ : β * x ^ 2 ≤ 2) : 0 < β ∧ β ≤ 1 / 16 ∧ 0 < √β ∧ √β ≤ 1 / 4 ∧ 1 / √β ≤ j ^ 2 * x / √β ∧ j ^ 2 * x / √β ≤ 2 * j ^ 2 * x ^ 2 ∧ 0 < 1 / (j ^ 2 * x) ∧ 1 / (j ^ 2 * x) ≤ 1 / 2

The actual quadratic target and frame invariant imply every basic small-beta and target-time guard used in the scalar ODE estimates.

theorem EulerPacketScaleActivation.source_activation_within_horizon {j x β C : ℝ} (hj : 3 ≤ j) (hx : 8 ≤ x) (hC : 2 ≤ C) (hβx : 1 / 2 ≤ β * x ^ 2) (hβx₂ : β * x ^ 2 ≤ 2) : 1 ≤ C * (1 + j ^ 2 * x ^ 2) ∧ j ^ 2 * x / √β ≤ C * (1 + j ^ 2 * x ^ 2) ∧ β * (j ^ 2 * x / √β) ^ 2 = (j ^ 2 * x) ^ 2

The source polynomial horizon contains the target activation time.

theorem EulerPacketSourceScaleGuards.actualTimeRatio_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : EulerPacketSourceScaleSequence.timeWidth J X (n + 1) / EulerPacketSourceScaleSequence.timeWidth J X n ≤ EulerPacketSourceTime.sourceTimeRatio J (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerPacketSourceScaleGuards.actualExtraTime_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) (a : ℝ) (ha : 0 ≤ a) : 2 * √(a * EulerPacketSourceScaleSequence.previousShear J X n) * EulerPacketSourceScaleSequence.timeWidth J X (n + 1) ≤ 2 * √(a * Real.exp (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 7)) * EulerPacketSourceTime.sourceNextTimeWidth J (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerPacketSourceScaleGuards.actualParentRatio_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 < X) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : EulerPacketSourceScaleSequence.previousShear J X n ^ 2 / EulerPacketSourceScaleSequence.shear J X n ≤ EulerPacketSourceScaleChoice.parentSquareRatio J (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerPacketSourceScaleGuards.actualGoodCost_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (n : ℕ) : EulerPacketSourceScaleSequence.spike J X n * EulerPacketSourceScaleSequence.shear J X n * EulerPacketSourceScaleSequence.previousShear J X n ≤ EulerPacketSourceScaleChoice.goodCost J (EulerPacketSourceScaleChoice.scaleSequence J X) n

noncomputable def EulerPacketSourceScaleGuards.actualExtraTime (J : ℕ) (X a : ℝ) (n : ℕ) : ℝ

Actual extra time, given by 2*sqrt (a*previousShear J X n)*timeWidth J X (n+1).

Equations

• EulerPacketSourceScaleGuards.actualExtraTime J X a n = 2 * √(a * EulerPacketSourceScaleSequence.previousShear J X n) * EulerPacketSourceScaleSequence.timeWidth J X (n + 1)

theorem EulerPacketSourceScaleGuards.actualExtraTime_small (J D : ℕ) (hJ : 3 ≤ J) (C c X δ : ℝ) (hC : 1 ≤ C) (hX : 8 ≤ X) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (n : ℕ) (a : ℝ) (ha : 0 ≤ a) (ha₂ : a ≤ 2) : actualExtraTime J X a n * EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n ^ 60 ≤ δ

theorem EulerPacketSourceScaleGuards.actualWidths_contract (J D : ℕ) (hJ : 3 ≤ J) (C c X δ : ℝ) (hX : 8 ≤ X) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (hδ : δ ≤ 1 / 2) (n : ℕ) : EulerPacketSourceScaleSequence.timeWidth J X (n + 1) ≤ EulerPacketSourceScaleSequence.timeWidth J X n / 2

theorem EulerPacketSourceScaleGuards.coefficient_small (J D : ℕ) (hJ : 3 ≤ J) (C c X δ : ℝ) (hC : 1 ≤ C) (hX : 8 ≤ X) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (a : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (A : ℕ) (hA : A ≤ 60) (n : ℕ) : EulerPacketSourceScaleActual.geometryError J D C c X a n * EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n ^ A ≤ δ

theorem EulerPacketSourceScaleGuards.compression_of_error_small {a ε Θ target G d : ℝ} (ha : 1 / 2 ≤ a) (hε : 0 ≤ ε) (hΘ : 0 ≤ Θ) (htarget : target ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (herr : 16 * (ε * Θ * (4 * G) ^ 2 + d) ≤ 1) : 60 * (G + d) * target * ε < a

The strong coefficient-error guard already implies compression domination; no independent scale choice is required for it.

theorem EulerPacketSourceScaleGuards.scaleSequence_ge_initial (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 0 ≤ X) (n : ℕ) : X ≤ EulerPacketSourceScaleChoice.scaleSequence J X n

noncomputable def EulerPacketSourceScaleGuards.targetTime (J : ℕ) (X β : ℝ) (n : ℕ) : ℝ

Target time, given by scaleSequence J X (n+1)/sqrt β.

Equations

• EulerPacketSourceScaleGuards.targetTime J X β n = EulerPacketSourceScaleChoice.scaleSequence J X (n + 1) / √β

noncomputable def EulerPacketSourceScaleGuards.horizon (J : ℕ) (X a β : ℝ) (n : ℕ) : ℝ

Horizon, given by targetTime J X β n+actualExtraTime J X a n.

Equations

• EulerPacketSourceScaleGuards.horizon J X a β n = EulerPacketSourceScaleGuards.targetTime J X β n + EulerPacketSourceScaleGuards.actualExtraTime J X a n

structure EulerPacketSourceScaleGuards.StageGuards (J D : ℕ) (C c X K : ℝ) (a β : ℕ → ℝ) (n : ℕ) : Prop

Stage guards data, collecting epsilon_pos, epsilon_small, sigma_pos, sigma_small, reciprocal_pos, reciprocal_small and their compatibility conditions.

• epsilon_pos : 0 < EulerPacketSourceScaleActual.epsilon J X (a n) n
• epsilon_small : EulerPacketSourceScaleActual.epsilon J X (a n) n ≤ 1
• sigma_pos : 0 < √(β n)
• sigma_small : √(β n) ≤ 1 / 4
• reciprocal_pos : 0 < (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1))⁻¹
• reciprocal_small : (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1))⁻¹ ≤ 1 / 2
• target_from_sigma : 1 / √(β n) ≤ targetTime J X (β n) n
• target_le_horizon : targetTime J X (β n) n ≤ horizon J X (a n) (β n) n
• horizon_le_Theta : horizon J X (a n) (β n) n ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n
• extra_time : horizon J X (a n) (β n) n - targetTime J X (β n) n ≤ 1 / EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n ^ 60
• next_width : EulerPacketSourceScaleSequence.timeWidth J X (n + 1) ≤ EulerPacketSourceScaleSequence.timeWidth J X n / 2
• geometry_small : 1000000 * K * EulerPacketSourceScaleActual.geometryError J D C c X a n * EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n ^ 40 ≤ 1
• compression : 60 * (1 + EulerPacketSourceScaleSequence.olderShear J X n + (EulerPacketSourceScaleActual.priorError J D X n + EulerPacketSourceScaleActual.neighborError J D X c n)) * targetTime J X (β n) n * EulerPacketSourceScaleActual.epsilon J X (a n) n < a n

theorem EulerPacketSourceScaleGuards.stage_guards (J D : ℕ) (hJ : 3 ≤ J) (C c X K δ : ℝ) (hC : 4 ≤ C) (hX : 8 ≤ X) (hK : 1 ≤ K) (hδ : δ ≤ 1 / 2) (hδK : 1000000 * K * δ ≤ 1) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (a β : ℕ → ℝ) (ha : ∀ (n : ℕ), 1 / 2 ≤ a n) (ha₂ : ∀ (n : ℕ), a n ≤ 2) (hβ : ∀ (n : ℕ), 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ₂ : ∀ (n : ℕ), β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) (n : ℕ) : StageGuards J D C c X K a β n

theorem EulerPacketSourceScaleGuards.exists_guarded_sequence (D : ℕ) (hD : 1000 ≤ D) (C c K : ℝ) (hC : 4 ≤ C) (hc : 0 ≤ c) (hK : 1 ≤ K) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (η : ℝ), 0 < η → ∃ (X₀ : ℝ) (δ : ℝ), 8 ≤ X₀ ∧ 0 < δ ∧ δ ≤ η ∧ ∀ (X : ℝ), X₀ ≤ X → EulerPacketSourceScaleActual.ActualBounds J D C c X δ ∧ ∀ (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 : ℕ), StageGuards J D C c X K a β n

All numerical geometry guards are achieved by one fixed stage, then one base scale, uniformly over every frame satisfying the induction invariants.

theorem EulerPacketSourceScaleGuards.parameter_packet_bound_eventually (J : ℕ) (hJ : 3 ≤ J) (X Cbase Cstar : ℝ) (hX : 1 ≤ X) (hCbase : 1 ≤ Cbase) (hCstar : 0 ≤ Cstar) (Q : ℕ) (θ : ℝ) (hθ : 0 < θ) : ∀ᶠ (n : ℕ) in Filter.atTop, EulerScale.sourceParameterAggregate J Cbase Cstar (EulerPacketSourceScaleChoice.scaleSequence J X) n ^ Q ≤ EulerPacketSourceScaleSequence.frequency J X n ^ θ

Equation (39) gives the actual packet power inequality for the constructed sequence, for every fixed polynomial degree and positive frequency exponent. The aggregate includes any fixed base constants.