Exact scale differences of actual velocity material powers.

theorem AVenhance.Infra.Section4.amnr_velocity_power_error_expansion {b c : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (n : ℕ) (i : Fin 2) : ((amnrWord b (List.replicate n none) fun (y : AmnrSpace) => b y i) - amnrWord c (List.replicate n none) fun (y : AmnrSpace) => c y i) = amnrWord c (List.replicate n none) (amnrAdvectionVelocity b c i) + amnrMaterialErrorValue b c (fun (y : AmnrSpace) => b y i) n

The material scale difference retains one coarse fast-velocity jet plus the explicit correction sum, with no factor on the pure coarse term.

theorem AVenhance.Infra.Section4.amnr_velocity_coarse_mixed_abs_le_of_bounds {b c : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (w : List (Option (Fin 2))) (i : Fin 2) (z : AmnrSpace) {A B : ℝ} (hcoarse : |amnrWord c w (fun (y : AmnrSpace) => c y i) z| ≤ A) (hfast : |amnrWord c w (amnrAdvectionVelocity b c i) z| ≤ B) : |amnrWord c w (fun (y : AmnrSpace) => b y i) z| ≤ A + B

Nonempty coarse canonical velocity jets split into actual coarse and fast jets; the scalar drift is never used in the estimate.