Explicit scalar choices for the actual drift-aware correction budget. The error target is exp(-sqrt X), with X=k^ϑ in the source construction.

noncomputable def EulerPacketCorrectionScalar.delta (X : ℝ) : ℝ

Delta, given by Real.exp (-Real.sqrt X).

Equations

• EulerPacketCorrectionScalar.delta X = Real.exp (-√X)

noncomputable def EulerPacketCorrectionScalar.residual (k X : ℝ) : ℝ

Residual, given by 2*Real.exp (-(7/10)*X*Real.log k).

Equations

• EulerPacketCorrectionScalar.residual k X = 2 * Real.exp (-(7 / 10) * X * Real.log k)

noncomputable def EulerPacketCorrectionScalar.initialRadius (R M Rc : ℝ) : ℝ

Initial radius, given by 1/(1+8*R+4*M*Rc+Rc).

Equations

• EulerPacketCorrectionScalar.initialRadius R M Rc = 1 / (1 + 8 * R + 4 * M * Rc + Rc)

theorem EulerPacketCorrectionScalar.delta_pos (X : ℝ) : 0 < delta X

theorem EulerPacketCorrectionScalar.delta_le_one (X : ℝ) : delta X ≤ 1

theorem EulerPacketCorrectionScalar.residual_pos (k X : ℝ) : 0 < residual k X

theorem EulerPacketCorrectionScalar.initialRadius_bounds (R M Rc : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (hRc : 0 ≤ Rc) : 0 < initialRadius R M Rc ∧ initialRadius R M Rc * (4 * R) ≤ 1 / 2 ∧ 4 * M * (initialRadius R M Rc * Rc) ≤ 1 ∧ initialRadius R M Rc * Rc ≤ 1

One polynomial inverse radius meets both packet-series and pressure - inverse absorption requirements.

theorem EulerPacketCorrectionScalar.residual_small (C T k X : ℝ) (hX : 64 ≤ X) (hk : 1 ≤ Real.log k) (hgrowth : 3 * C * T ≤ X / 4) : 2 * residual k X * Real.exp (3 * C * T) ≤ delta X / 2

The actual residual envelope wins over the Gronwall factor with an explicit linear bound on the source growth cost.

theorem EulerPacketCorrectionScalar.radius_decay (C T D ρ0 k X : ℝ) (hk : 0 < k) (hfrequency : 8 * C * T * D ≤ ρ0 * k) (herror : 8 * C * T ≤ ρ0 * Real.exp √X) : 2 * C * (D / k + delta X) * T ≤ ρ0 / 2

The two elementary frequency guards control the radius loss caused by the actual O(1/k) drift and the chosen error target.

noncomputable def EulerPacketCorrectionScalar.radius (T C D ρ0 k X : ℝ) : C(↑(Set.Icc 0 T), ℝ)

Radius, given by ⟨fun t => ρ0-2*C*(D/k+delta X)*t.val, continuous_const.sub (continuous_const.mul continuous_subtype_val)⟩.

Equations

• EulerPacketCorrectionScalar.radius T C D ρ0 k X = { toFun := fun (t : ↑(Set.Icc 0 T)) => ρ0 - 2 * C * (D / k + EulerPacketCorrectionScalar.delta X) * ↑t, continuous_toFun := ⋯ }

theorem EulerPacketCorrectionScalar.radius_bounds (T C D ρ0 k X : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hk : 0 < k) (hdecay : 2 * C * (D / k + delta X) * T ≤ ρ0 / 2) (t : ↑(Set.Icc 0 T)) : ρ0 / 2 ≤ (radius T C D ρ0 k X) t ∧ (radius T C D ρ0 k X) t ≤ ρ0