Packet Uniform Scale Sums

theorem EulerPacketUniformScaleSums.polynomial_scale_doubles (J A : ℕ) (hJ : 1 ≤ J) (hJA : 2 ^ (A + 1) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (n : ℕ) : 2 * (x n / ↑(J + n) ^ A) ≤ x (n + 1) / ↑(J + (n + 1)) ^ A

Once the initial stage dominates the fixed polynomial exponent, the rescaled quadratic sequence grows by at least a factor two at every step.

theorem EulerPacketUniformScaleSums.polynomial_scale_geometric_lower (J A : ℕ) (hJ : 1 ≤ J) (hJA : 2 ^ (A + 1) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (n : ℕ) : 2 ^ n * (x 0 / ↑J ^ A) ≤ x n / ↑(J + n) ^ A

The entire positive exponent sequence is bounded below by its first term times 2^n, uniformly in the initial scale.

theorem EulerPacketUniformScaleSums.stage_count_le_two_pow (n : ℕ) : ↑n + 1 ≤ 2 ^ n

A simple exact comparison between binary growth and the stage count.

theorem EulerPacketUniformScaleSums.source_exponential_geometric_majorant (J A : ℕ) (hJ : 1 ≤ J) (hJA : 2 ^ (A + 1) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (b : ℝ) (hb : 0 < b) (n : ℕ) : Real.exp (-b * (x n / ↑(J + n) ^ A)) ≤ Real.exp (-b * (x 0 / ↑J ^ A)) * Real.exp (-b * (x 0 / ↑J ^ A)) ^ n

Every term of the source exponential series is bounded by one explicit geometric series whose ratio depends only on the first scale.

theorem EulerPacketUniformScaleSums.source_exponential_tsum_bound (J A : ℕ) (hJ : 1 ≤ J) (hJA : 2 ^ (A + 1) ≤ ↑J ^ 2) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (b : ℝ) (hb : 0 < b) : ∑' (n : ℕ), Real.exp (-b * (x n / ↑(J + n) ^ A)) ≤ Real.exp (-b * (x 0 / ↑J ^ A)) / (1 - Real.exp (-b * (x 0 / ↑J ^ A)))

The full exponential-cost sum has an explicit upper bound tending to zero as the initial scale increases. This makes the uniform small-sum choice in the source quantitative.

theorem EulerPacketUniformScaleSums.source_exponential_bound_tendsto_zero (J A : ℕ) (hJ : 1 ≤ J) (b : ℝ) (hb : 0 < b) : Filter.Tendsto (fun (X : ℝ) => Real.exp (-b * (X / ↑J ^ A)) / (1 - Real.exp (-b * (X / ↑J ^ A)))) Filter.atTop (nhds 0)

The explicit geometric-series bound vanishes as x₀ tends to infinity.