Scalar rate bookkeeping for the p.Hm and p.dm interfaces.

The geometric factors retain the corrected exponent 4δ and the cutoff Jcut. The helpers in this file keep the temperature amplitude as a scalar parameter.

theorem AVenhance.Infra.Section4.hm_dm_jcut_power_budget {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 2 + gamma β ≤ delta β * ↑(Jcut β) / 2

The corrected cutoff is long enough to absorb the fixed negative power in the Jcut remainder scale.

theorem AVenhance.Infra.Section4.HmDmScales.hmDm_rpow_square {E p : ℝ} (hE : 0 < E) : (E ^ p) ^ 2 = E ^ (2 * p)

theorem AVenhance.Infra.Section4.dm_tail_scale_from_rate_bounds {β : ℝ} (I : Ingredients β) (m J : ℕ) {E δ γ C₀ Csrc Cprod Theta κm κprev epsm tau tauP A Khalf Afac x : ℝ} (hE : 0 < E) (hE1 : E ≤ 1) (_hδ : 0 < δ) (_hγ : 0 ≤ γ) (hC₀ : 0 ≤ C₀) (hCsrc : 0 ≤ Csrc) (hCprod : 0 ≤ Cprod) (hTheta : 0 ≤ Theta) (_hκm : 0 < κm) (hκprev : 0 < κprev) (hepsm : 0 < epsm) (htau : 0 < tau) (htauP : 0 < tauP) (hKhalf : Khalf = √κprev * Theta) (hAfac : Afac = 2) (hx : x = E ^ (δ / 2)) (hProduct : a β I.Λ m ^ 2 * epsm ^ 4 / κm ≤ Cprod * κprev) (hTimeRatio : tau / tauP ≤ 1 / 4 * E ^ δ) (hPower : 2 + γ ≤ δ * ↑J / 2) (hA : 0 ≤ A ∧ A ≤ Csrc * Theta * (epsm ^ 2 / κm) * (√κprev)⁻¹ * E ^ (-(2 + γ)) * tauP⁻¹ ^ J) : ↑(Nstar β) * (8 * A * (4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsm ^ 2) * (8 * tau) ^ J)) ≤ ↑(Nstar β) * (8 * (4 * Real.pi ^ 2 * C₀) * Csrc * Cprod) * Khalf * (Afac * x) ^ J

The terminal Jcut tensor remainder has the scale once its termwise AMNR envelope, product bound, and time-ratio bound are inserted. The exponent loss 2+γ is paid by the exact Jcut budget.

theorem AVenhance.Infra.Section4.HmDmScales.hmDm_abs_apply_le_sqrt_vecNormSq (v : Homogenization.Vec 2) (i : Fin 2) : |v i| ≤ √(Homogenization.vecNormSq v)

theorem AVenhance.Infra.Section4.HmDmScales.hmDm_continuous_vecNormSq : Continuous fun (v : Homogenization.Vec 2) => Homogenization.vecNormSq v