Packet Base Scales

theorem EulerPacketBaseScales.base_power_decay (T p : ℝ) (m k : ℕ) (hp : p + 2 * ↑m + ↑k < 0) : Filter.Tendsto (fun (x : ℝ) => x ^ p * (T * x ^ 2) ^ m * x ^ k) Filter.atTop (nhds 0)

A negative total real power absorbs a fixed monomial horizon.

theorem EulerPacketBaseScales.base_exponential_decay (T p b : ℝ) (m k : ℕ) (hb : 0 < b) : Filter.Tendsto (fun (x : ℝ) => x ^ p * Real.exp (-b * x) * (T * x ^ 2) ^ m * x ^ k) Filter.atTop (nhds 0)

Exponential decay absorbs every fixed real polynomial power and every fixed monomial horizon power.

theorem EulerPacketBaseScales.first_stage_coefficient_error_tendsto_zero (T D N b : ℝ) (hD : 1000 ≤ D) (hb : 0 < b) : Filter.Tendsto (fun (x : ℝ) => 16 * (8 * x ^ (-500) * (T * x ^ 2) + x ^ (-D / 4) + x ^ N * Real.exp (-b * x)) * (T * x ^ 2) ^ 60 * x ^ 10) Filter.atTop (nhds 0)

The first normal stage has h=x₀^1000, hence epsilon of order x₀^-500; its complete coefficient error beats x₀^-10 Θ^-60.

theorem EulerPacketBaseScales.second_stage_shear_error_tendsto_zero (T b : ℝ) (hb : 0 < b) (A : ℕ) : Filter.Tendsto (fun (x : ℝ) => Real.exp (-b * x) * (1 + x ^ 1000) ^ 2 * (T * x ^ 2) ^ A) Filter.atTop (nhds 0)

At the special second stage the older gradient is polynomial in the base scale, while the new inverse shear is exponentially small.

theorem EulerPacketBaseScales.base_horizon_tendsto_zero (J : ℝ) : Filter.Tendsto (fun (x : ℝ) => 6 * J ^ 2 * x ^ (2 - 1000 / 2)) Filter.atTop (nhds 0)

The exact base horizon 6 J² x₀^(2-1000/2) tends to zero.

theorem EulerPacketBaseScales.base_core_volume_cost_tendsto_zero (J : ℝ) : Filter.Tendsto (fun (x : ℝ) => x ^ 1000 * (x ^ (-1000)) ^ 3 * (6 * J ^ 2 * x ^ (-498))) Filter.atTop (nhds 0)

The core-volume guard h r³ Sbase, with r=x₀^-1000, also tends to zero from the explicit base choices.