Quantitative material/spatial commutation for arbitrary outer words.

theorem AVenhance.Infra.Section4.amnr_word_material_spatial_abs_le_of_bounds {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (w : List (Option (Fin 2))) (i : Fin 2) (z : AmnrSpace) {S H F B G : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hB : 0 ≤ B) (hG : 0 ≤ G) (hF : |amnrWord b (w ++ [some i, none]) f z| ≤ F) (hBb : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → |amnrWord b v (amnrVelocityGradient b p i) z| ≤ B * amnrWeight S H v) (hGb : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → |amnrWord b v (amnrOp b (some p) f) z| ≤ G * amnrWeight S H v) : |amnrWord b w (amnrOp b none (amnrOp b (some i) f)) z| ≤ F + 2 ^ (w.length + 1) * B * G * amnrWeight S H w

Every outer word can be applied to the actual material/spatial commutator; complementary subwords control each product factor.