The previous-diffusivity normalization retained in the Hm gradient calculation. This conditional source-scale helper sharpens the public sqrt(kappa_m) conclusion to sqrt(kappa_{m-1}), for signed flux pairing.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_gradient_sharp_of_amnr_scales
{β C₀ CA K C ν S : ℝ}
(hCA : 0 ≤ CA)
(hS : 0 ≤ S)
(hK : 0 ≤ K)
(hC : 0 ≤ C)
(I : Ingredients β)
(hz : I.Czeta ≤ C₀)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κ : ℝ}
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hκ : 0 < κ)
(hκν : κ ≤ ν)
(hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1)
(hτ : 8 * tau β I.Λ m / tauP β I.Λ m ≤ 1 / 2)
(hX : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ K * ν)
(hν : ν ≤ C * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)))
(hat : a β I.Λ (m - 1) * tau β I.Λ m ≤ 2 ^ (-28) * epsilon β I.Λ (m - 1) ^ (4 * delta β))
(hHessEntryMeas :
∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k p : Fin 2),
MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p)
(MeasureTheory.volume.restrict timeCube))
(hGradientMeas :
∀ r ∈ Finset.range (Jcut β),
MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2)
(MeasureTheory.volume.restrict timeCube))
(hD1 :
∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k : Fin 2) (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2),
DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x)
(hD2 :
∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k : Fin 2) (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2),
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i)
x)
(hHmrD :
∀ r ∈ Finset.range (Jcut β),
∀ (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x)
(hAmnr :
∀ r₀ ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
MeasureTheory.eLpNorm (Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r₀) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal
(CA * S * (epsilon β I.Λ m ^ 2 / κ) / √ν * (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ 2 * (tauP β I.Λ m)⁻¹ ^ r₀))
:
The source-scale calculation supports the previous diffusivity in front of the gradient norm. All upstream AMNR and regularity inputs stay explicit.