Parent-independent frequency margins. Once every source cost is below the same tiny power, these margins yield both small physical errors and the genuine small-velocity flow guard.

The actual correction target absorbs every fixed power of the frequency.

theorem EulerPacketSourceFrequency.sqrt_expansion_eq (k : ℝ) (hk : 0 ≤ k) : √(expansion k) = k ^ (theta / 2)

theorem EulerPacketSourceFrequency.delta_mul_rpow_tendsto_zero (p : ℝ) : Filter.Tendsto (fun (k : ℝ) => k ^ p * EulerPacketCorrectionScalar.delta (expansion k)) Filter.atTop (nhds 0)

The target from the actual scalar construction decays faster than every fixed inverse power; no rate is assumed as a separate hypothesis.

theorem EulerPacketSourceFrequency.correction_eventually_lt_inverse_power (C p : ℝ) : ∀ᶠ (k : ℝ) in Filter.atTop, C * EulerPacketCorrectionScalar.delta (expansion k) < k ^ (-p)

Any fixed source multiplier is eventually smaller than an arbitrary fixed inverse power of the frequency.

theorem EulerPacketSourceFrequency.correction_with_power_loss_eventually (C loss p : ℝ) : ∀ᶠ (k : ℝ) in Filter.atTop, C * k ^ loss * EulerPacketCorrectionScalar.delta (expansion k) < k ^ (-p)

Fixed polynomial losses from physical differentiation or graph restriction are absorbed by the same actual correction target.

The literal correction target and a fixed inverse-frequency packet amplitude give the small lifted velocity required by the finite flow bootstrap. All source constants remain fixed as frequency increases.

noncomputable def EulerPacketSourceFrequency.liftedAmplitude (C E k : ℝ) : ℝ

Lifted amplitude, given by C/k + E*delta (expansion k).

Equations

• EulerPacketSourceFrequency.liftedAmplitude C E k = C / k + E * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)

theorem EulerPacketSourceFrequency.fixed_div_eventually_le_inverse_half (C : ℝ) : ∀ᶠ (k : ℝ) in Filter.atTop, C / k ≤ k ^ (-(1 / 2))

theorem EulerPacketSourceFrequency.liftedAmplitude_nonneg (C E k : ℝ) (hC : 0 ≤ C) (hE : 0 ≤ E) (hk : 0 ≤ k) : 0 ≤ liftedAmplitude C E k

theorem EulerPacketSourceFrequency.liftedAmplitude_eventually_le_inverse_half (C E : ℝ) : ∀ᶠ (k : ℝ) in Filter.atTop, liftedAmplitude C E k ≤ 2 * k ^ (-(1 / 2))

theorem EulerPacketSourceFrequency.liftedAmplitude_small_eventually (C E R T : ℝ) (hC : 0 ≤ C) (hE : 0 ≤ E) (hR : 0 ≤ R) (hT : 0 ≤ T) : ∀ᶠ (k : ℝ) in Filter.atTop, 4 ≤ k ∧ 0 ≤ liftedAmplitude C E k ∧ liftedAmplitude C E k ≤ 2 * k ^ (-(1 / 2)) ∧ liftedAmplitude C E k * R * T ≤ 1 / 8

theorem EulerPacketSourceFrequency.smallPower_le_power (k p : ℝ) (hk : 1 ≤ k) (hp : theta / 100 ≤ p) : smallPower k ≤ k ^ p

theorem EulerPacketSourceFrequency.cost_div_le_inverse_half (C k : ℝ) (hk : 1 ≤ k) (hC : C ≤ smallPower k) : C / k ≤ k ^ (-(1 / 2))

theorem EulerPacketSourceFrequency.cost_delta_le (C k : ℝ) (hk : 1 ≤ k) (hC : C ≤ smallPower k) (hd : EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-3)) : C * EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-(5 / 2))

theorem EulerPacketSourceFrequency.cost_frequency_delta_le_inverse_half (C k : ℝ) (hk : 1 ≤ k) (hC : C ≤ smallPower k) (hd : EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-3)) : C * k * EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-(1 / 2))

theorem EulerPacketSourceFrequency.physical_error_le_inverse_quarter (C E k : ℝ) (hk : 1 ≤ k) (hC : C ≤ smallPower k) (hE : E ≤ smallPower k) (hd : EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-3)) (hroot : 2 ≤ k ^ (1 / 4)) : C / k + E * k * EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-(1 / 4))

theorem EulerPacketSourceFrequency.liftedAmplitude_small_of_costs (C E R T k : ℝ) (hk : 1 ≤ k) (hR : 0 ≤ R) (hT : 0 ≤ T) (hC : C ≤ smallPower k) (hE : E ≤ smallPower k) (hRw : R ≤ smallPower k) (hTw : T ≤ smallPower k) (hd : EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-3)) (hroot : 16 ≤ k ^ (1 / 4)) : liftedAmplitude C E k ≤ 2 * k ^ (-(1 / 2)) ∧ liftedAmplitude C E k * R * T ≤ 1 / 8

theorem EulerPacketSourceFrequency.universal_margin_eventually (K : ℝ) : ∀ᶠ (k : ℝ) in Filter.atTop, 4 ≤ k ∧ 64 ≤ expansion k ∧ 1 ≤ Real.log k ∧ EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-3) ∧ 16 ≤ k ^ (1 / 4) ∧ max 71 K ≤ k ^ (1 / 24)

This one numerical threshold is independent of all parent fields, all source costs and all stages of the iteration.