Packet Scale Geometry

theorem EulerPacketScaleGeometry.activation_time_bounds {a β H x X : ℝ} (ha : 1 / 2 ≤ a) (ha₂ : a ≤ 2) (hH : 0 < H) (hx : 0 < x) (hX : 0 ≤ X) (hβx : 1 / 2 ≤ β * x ^ 2) (hβx₂ : β * x ^ 2 ≤ 2) : 3 * X * x / √H / 6 ≤ X / √(β * a * H) ∧ X / √(β * a * H) ≤ 2 * (3 * X * x / √H) / 3

The activation-time interval in (38) follows from the two frame invariants in (24), with the numerical constants stated in the source.

theorem EulerPacketScaleGeometry.nested_horizon_of_width_ratio {t Δ W Wnext : ℝ} (hW : 0 ≤ W) (hΔ : Δ ≤ 2 * W / 3) (hnext : Wnext ≤ W / 2) : t + Δ + 2 * Wnext ≤ t + 2 * W

A sufficiently small next time width makes the packet horizons nest.

theorem EulerPacketScaleGeometry.stage_power_div_predecessor_power_tendsto_zero (J : ℕ) (hJ : 2 ≤ J) (A B : ℕ) (hAB : A < B) : Filter.Tendsto (fun (n : ℕ) => ↑(J + n) ^ A / ↑(J - 1 + n) ^ B) Filter.atTop (nhds 0)

Powers of a shifted stage index divided by a larger predecessor power vanish, a basic consequence of the quadratic recurrence geometry.

theorem EulerPacketScaleGeometry.polynomial_exponential_decay_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A p q : ℕ) (C b : ℝ) (hC : 0 < C) (hb : 0 < b) : Summable fun (n : ℕ) => C * ↑(J + n) ^ p * x n ^ q * Real.exp (-b * (x n / ↑(J + n) ^ A))

Exponential decay on any polynomially rescaled quadratic scale absorbs every fixed polynomial in the scale and the stage index.

theorem EulerPacketScaleGeometry.stage_div_shifted_tendsto_one (J d : ℕ) (hJ : d < J) : Filter.Tendsto (fun (n : ℕ) => ↑(J + n) / ↑(J - d + n)) Filter.atTop (nhds 1)

The ratio of a stage to any fixed predecessor tends to one.

theorem EulerPacketScaleGeometry.stage_rpow_div_shifted_power_tendsto_zero (J d B : ℕ) (hJ : d < J) (A : ℝ) (hAB : A < ↑B) : Filter.Tendsto (fun (n : ℕ) => ↑(J + n) ^ A / ↑(J - d + n) ^ B) Filter.atTop (nhds 0)

A real power below a predecessor's natural power has vanishing ratio; this includes the source's support exponent 7/2.

theorem EulerPacketScaleGeometry.polynomial_log_relative_tendsto_zero (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A C p q : ℝ) (_hA : 0 ≤ A) : Filter.Tendsto (fun (n : ℕ) => (C + p * Real.log ↑(J + n) + q * Real.log (x n)) / (x n / ↑(J + n) ^ A)) Filter.atTop (nhds 0)

Polynomial logarithms are negligible relative to x/j^A, for every nonnegative real exponent A.

theorem EulerPacketScaleGeometry.source_scale_exponential_summable (J d B : ℕ) (hJ : d < J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A b c C p q : ℝ) (hA : 0 ≤ A) (hAB : A < ↑B) (hb : 0 < b) : Summable fun (n : ℕ) => Real.exp (-b * (x n / ↑(J + n) ^ A) + c * (x n / ↑(J - d + n) ^ B) + C + p * Real.log ↑(J + n) + q * Real.log (x n))

Explicit positive logarithmic errors from older stages are absorbed by the source's negative exponential scale. No smallness guard is assumed.