Quantitative mixed jets for a two-dimensional matrix product.

theorem AVenhance.Infra.Section4.amnrWord_add_contDiffOn {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} {N : ℕ} (hb : ContDiffOn ℝ (↑N) b U) (hf : ContDiffOn ℝ (↑N) f U) (hg : ContDiffOn ℝ (↑N) g U) (w : List (Option (Fin 2))) (hw : w.length ≤ N) : Set.EqOn (amnrWord b w (f + g)) (amnrWord b w f + amnrWord b w g) U

Addition commutes with finite smoothness words at every point of an open set. This upstream version lets coefficient estimates stay below the flux modules in the import graph.

theorem AVenhance.Infra.Section4.amnr_matrix_product_sub_const_word_bound {b : AmnrSpace → Homogenization.Vec 2} {N : ℕ} {K G : Fin 2 → AmnrSpace → ℝ} (hb : ContDiff ℝ (↑N) b) (hK : ∀ (p : Fin 2), ContDiff ℝ (↑N) (K p)) (hG : ∀ (p : Fin 2), ContDiff ℝ (↑N) (G p)) {S H A B d : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hA : 0 ≤ A) (hB : 0 ≤ B) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ N) (hKb : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (z : AmnrSpace), |amnrWord b v (K p) z| ≤ A * amnrWeight S H v) (hGb : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (z : AmnrSpace), |amnrWord b v (G p) z| ≤ B * amnrWeight S H v) (z : AmnrSpace) : |amnrWord b w (fun (y : AmnrSpace) => ∑ p : Fin 2, K p y * G p y - d) z| ≤ (2 * 2 ^ N * A * B + |d|) * amnrWeight S H w

A finite matrix contraction preserves the weighted mixed budget. This conditional calculus helper accounts for all product-rule terms explicitly.

theorem AVenhance.Infra.Section4.amnr_matrix_double_product_word_bound {b : AmnrSpace → Homogenization.Vec 2} {N : ℕ} {P H : Fin 2 → Fin 2 → AmnrSpace → ℝ} (hb : ContDiff ℝ (↑N) b) (hP : ∀ (i p : Fin 2), ContDiff ℝ (↑N) (P i p)) (hH : ∀ (i p : Fin 2), ContDiff ℝ (↑N) (H i p)) {S T A B : ℝ} (hS : 0 ≤ S) (hT : 0 ≤ T) (hA : 0 ≤ A) (hB : 0 ≤ B) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ N) (hPb : ∀ (i p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (z : AmnrSpace), |amnrWord b v (P i p) z| ≤ A * amnrWeight S T v) (hHb : ∀ (i p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (z : AmnrSpace), |amnrWord b v (H i p) z| ≤ B * amnrWeight S T v) (z : AmnrSpace) : |amnrWord b w (fun (y : AmnrSpace) => ∑ i : Fin 2, ∑ p : Fin 2, P i p y * H i p y) z| ≤ 4 * 2 ^ N * A * B * amnrWeight S T w

A two-by-two contraction with two indexed factors costs one Leibniz factor per contracted row.

theorem AVenhance.Infra.Section4.amnr_word_sub_const_abs_le {b : AmnrSpace → Homogenization.Vec 2} {N : ℕ} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑N) b) (hf : ContDiff ℝ (↑N) f) {S T A c : ℝ} (hS : 0 ≤ S) (hT : 0 ≤ T) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ N) (z : AmnrSpace) (hbound : |amnrWord b w f z| ≤ A * amnrWeight S T w) : |amnrWord b w (fun (y : AmnrSpace) => f y - c) z| ≤ (A + |c|) * amnrWeight S T w

Subtracting a scalar constant adds its absolute size to a weighted word bound; every nonempty word annihilates the constant.