Finite telescoping for source-style material derivatives.

theorem AVenhance.Infra.Section5.finite_material_sum_telescope (J : ℕ) (U B : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (Dt : ℕ → ℝ) (LH : ℕ → Homogenization.Vec 2 →L[ℝ] ℝ) (t : ℝ) (x : Homogenization.Vec 2) (hDt : ∀ r ∈ Finset.range J, HasDerivAt (fun (s : ℝ) => U r s x) (Dt r) t) (hDx : ∀ r ∈ Finset.range J, HasFDerivAt (U r t) (LH r) x) (hstep : ∀ r ∈ Finset.range J, Dt r + (LH r) (b t x) = B (r + 1) t x - B r t x) : deriv (fun (s : ℝ) => ∑ r ∈ Finset.range J, U r s x) t + (fderiv ℝ (fun (y : Homogenization.Vec 2) => ∑ r ∈ Finset.range J, U r t y) x) (b t x) = B J t x - B 0 t x

If each summand's material derivative is the next minus current endpoint potential, the material derivative of the finite sum is the terminal minus initial potential. For the source, the summands are H_{m,r} and the potentials are div Σ_n A_{m,n,r} q_{m,n,r}; proving their per-index rule from the A and q recursions remains source-specific work.