Actual target amplification and the resulting exponential gain for bounded history sizes and the packet amplitude chosen at target.

theorem EulerPacketMovingFrame.equation30_target_exp_le {σ T Θ : ℝ} {Z Z₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hTtarget : 1 / σ ≤ T) (hTΘ : T ≤ Θ) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) : Real.exp (1 / (4 * σ)) ≤ Θ * Z T

theorem EulerPacketMovingFrame.physical_target_exponential_lower (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε σ T Θ : ℝ} {Z Z₁ : ℝ → ℝ} (hs₀ : 0 < s₀) (hε : ε ≠ 0) (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hTtarget : 1 / σ ≤ T) (hTΘ : T ≤ Θ) (hm : m (physicalTime t₀ a ε T) ≠ 0) (hv : v (physicalTime t₀ a ε T) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε T)) (v (physicalTime t₀ a ε T)) = 0) (hN : 1 / 2 ≤ scaledRay m v r s₀ t₀ a ε T 2) (hV : |scaledVelocity m v w t₀ a ε T 1 / Z T - 1| ≤ 1 / 2) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) : 0 < ‖r (physicalTime t₀ a ε T)‖ * ‖w (physicalTime t₀ a ε T)‖ ∧ s₀ * Real.exp (1 / (4 * σ)) ≤ 4 * Θ * (‖r (physicalTime t₀ a ε T)‖ * ‖w (physicalTime t₀ a ε T)‖)

theorem EulerPacketMovingFrame.ratio_bound_from_target_growth {s₀ Θ x target value bound : ℝ} (hs₀ : 0 < s₀) (hΘ : 0 < Θ) (hbound : 0 ≤ bound) (hvalue : value ≤ bound) (hgrowth : s₀ * Real.exp x ≤ 4 * Θ * target) : 0 < target ∧ value / target ≤ 4 * Θ * bound / s₀ * Real.exp (-x)

A bounded physical history size, or the numerator used to choose a packet amplitude, gains the actual target's exponential factor.