Physical spatial and material rates used by the mixed AMNR estimates.

theorem AVenhance.Infra.Section4.amnrWeight_mono {S₁ H₁ S₂ H₂ : ℝ} (hS₁ : 0 ≤ S₁) (hH₁ : 0 ≤ H₁) (hS : S₁ ≤ S₂) (hH : H₁ ≤ H₂) (w : List (Option (Fin 2))) : amnrWeight S₁ H₁ w ≤ amnrWeight S₂ H₂ w

Ordered radius products are monotone in both nonnegative rates.

theorem AVenhance.Infra.Section4.amnr_spatial_rate_le {E γ : ℝ} (hE : 0 < E) (hE1 : E ≤ 1) (hγ : 0 ≤ γ) : E⁻¹ ≤ E ^ (-(1 + γ / 2))

Abstract rpow comparison for the source's enlarged spatial radius.

theorem AVenhance.Infra.Section4.amnr_physical_rates {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : (epsilon β I.Λ (m - 1))⁻¹ ≤ epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2)) ∧ a β I.Λ (m - 1) ≤ (tauP β I.Λ m)⁻¹

The original flow rates are dominated by the actual AMNR radii.

theorem AVenhance.Infra.Section4.amnr_cutoff_window_fits_flow {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : tauPP β I.Λ m / 2 + tauP β I.Λ m ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹

The whole closed large-cutoff support window lies inside the short-flow interval required by the source flow derivative estimates.

theorem AVenhance.Infra.Section4.amnr_material_rate_small {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : a β I.Λ (m - 1) ≤ 2 ^ (-27) * epsilon β I.Λ (m - 1) ^ (3 * delta β) * (tauP β I.Λ m)⁻¹

The material cascade retains its source smallness factor. This stronger comparison is needed before absorbing constants in the temperature estimate.