Frequency guards turn the finite geometric remainder into fixed polynomial bounds.

theorem EulerPacketFiniteFrequency.fourth_power_le_frequency (k B : ℝ) (hk : 1 ≤ k) (hB0 : 0 ≤ B) (hB : B ≤ k ^ (1 / 100)) : B ^ 4 ≤ k

theorem EulerPacketFiniteFrequency.normalized_low_high_le (k B C₁ C₂ : ℝ) (hk : 2 ≤ k) (hC₂ : 0 ≤ C₂) (hB4 : B ^ 4 ≤ k) : k * (k⁻¹ * C₁ + k⁻¹ ^ 2 * C₂ + 2 * B * (k⁻¹ * B) ^ 3) ≤ C₁ + C₂ + 1

theorem EulerPacketFiniteFrequency.remainder_low_high_le (k B C₂ : ℝ) (hk : 0 < k) (hB4 : B ^ 4 ≤ k) : k⁻¹ ^ 2 * C₂ + 2 * B * (k⁻¹ * B) ^ 3 ≤ (C₂ + 2) / k ^ 2