Quantitative bounds for finite actual correction sums.

theorem AVenhance.Infra.Section4.amnr_list_abs_sum_le {α : Type u_1} (T : List α) (f : α → ℝ) {K : ℝ} (hT : ∀ t ∈ T, |f t| ≤ K) : |(List.map f T).sum| ≤ ↑T.length * K

theorem AVenhance.Infra.Section4.amnrMaterialError_spatial_abs_le_of_word_bounds {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {S H V C F : ℝ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hC : 1 ≤ C) (hF : 0 ≤ F) (hVS : V * S = H) (α : List (Fin 2)) (n : ℕ) (z : AmnrSpace) (hv : ∀ (p : Fin 2) (w : List (Option (Fin 2))), amnrMaterialCount w < n → amnrBudget w + 2 ≤ α.length + 2 * n → |amnrWord c w (amnrAdvectionVelocity b c p) z| ≤ C * V * amnrWeight S H w) (hscalar : ∀ (w : List (Option (Fin 2))), w ≠ [] → amnrMaterialCount w < n → amnrBudget w + 1 ≤ α.length + 2 * n → |amnrWord c w f z| ≤ F * V * amnrWeight S H w) : |amnrWord c (List.map some α) (amnrMaterialErrorValue b c f n) z| ≤ ↑(amnrMaterialErrorCardinality n * (n + 1) ^ α.length) * (C ^ n * F * V * S ^ α.length * H ^ n)

The error sum uses only strictly lower material jets, with their precise weighted budgets. This is a conditional calculus estimate, not a source premise.