The actual diffusivity step controls Kmat also at the terminal scale.

theorem AVenhance.Infra.Section4.amnr_kappa_previous_eq_step {β κ : ℝ} (I : Ingredients β) {m M : ℕ} (hm : 1 ≤ m) (hmM : m ≤ M) : I.kappaAt κ (m - 1) (M - (m - 1)) = I.KhomScalar (I.kappaAt κ m (M - m)) m

The exact diffusivity recursion, including the terminal step.

theorem AVenhance.Infra.Section4.amnr_kappa_step_size_of_averaging {β C₀ κ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) (hκ : 0 < κ) (hsmall : Section3.lAmtOneStepConstant β C₀ * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) + epsilon β I.Λ (m - 1) ^ delta β) ≤ 9 / 160) : κ + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ 160 / 9 * I.KhomScalar κ m

Smallness in the proved one-step averaging error yields a uniform size comparison without an invalid upper diffusivity-recursion bound at the terminal index.