Higher material scale steps with strictly lower canonical inputs.

theorem AVenhance.Infra.Section4.amnr_velocity_higher_step_abs_le_of_lower_bounds {b c : AmnrSpace → Homogenization.Vec 2} {S H V Cv Cc Cb Ct : ℝ} {N : ℕ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hCv : 1 ≤ Cv) (hCc : 0 ≤ Cc) (hCb : 0 ≤ Cb) (hVS : V * S = H) (α : List (Fin 2)) (n : ℕ) (hn : 1 ≤ n) (hbudget : α.length + 2 * n ≤ N) (i : Fin 2) (z : AmnrSpace) (hfast : ∀ (p : Fin 2) (η : List (Fin 2)) (r : ℕ), η.length + 2 * r + 1 ≤ N → r < n → |amnrWord c (amnrMixedWord η r) (amnrAdvectionVelocity b c p) z| ≤ Cv * V * amnrWeight S H (amnrMixedWord η r)) (hcoarse : ∀ (p : Fin 2) (η : List (Fin 2)) (r : ℕ), amnrMixedWord η r ≠ [] → η.length + 2 * r + 1 ≤ N → r < n → |amnrWord c (amnrMixedWord η r) (fun (y : AmnrSpace) => c y p) z| ≤ Cc * V * amnrWeight S H (amnrMixedWord η r)) (hB : ∀ (p j : Fin 2) (η : List (Fin 2)), ∀ r < n, η.length + 2 * r + 2 ≤ N → |amnrWord c (amnrMixedWord η r) (amnrVelocityGradient c p j) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord η r)) (htop : |amnrWord c (amnrMixedWord α n) (amnrAdvectionVelocity b c i) z| ≤ Ct * V * S ^ α.length * H ^ n) : |amnrWord c (List.map some α) ((amnrWord b (List.replicate n none) fun (y : AmnrSpace) => b y i) - amnrWord c (List.replicate n none) fun (y : AmnrSpace) => c y i) z| ≤ (Ct + ↑(amnrMaterialErrorCardinality n * (n + 1) ^ α.length) * (amnrNormalOrderConstant (N - 1) Cb (N - 1) * Cv) ^ n * (amnrNormalOrderConstant (N - 1) Cb (N - 1) * (Cc + Cv))) * V * S ^ α.length * H ^ n

Conditional induction step for the actual velocity scale difference. Only the transported fast term is at the current material level. Every changed-advection correction uses the strictly lower canonical inputs.