The finite material-derivative expansion instantiated on the locally finite cutoff ansatz.

theorem AVenhance.Infra.Section5.FrozenAnsatzMaterial.xiMK_eq_zero_off_nearSupport {β : ℝ} (I : Ingredients β) (m : ℕ) (t ρ s : ℝ) (hs : s ∈ Set.Ioo (t - ρ) (t + ρ)) {k : ℤ} (hk : k ∉ xiMKNearSupportFinset I m t ρ) : I.xiMK m k s = 0

theorem AVenhance.Infra.Section5.frozen_ansatz_material_expansion {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (ρ t : ℝ) (x b : Homogenization.Vec 2) (Tt Ht : ℝ) (ξt : ℤ → ℝ) (χt Gt : ℤ → Homogenization.Vec 2) (LT LH : Homogenization.Vec 2 →L[ℝ] ℝ) (Lχ LG : ℤ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (hρ : 0 < ρ) (hTt : HasDerivAt (fun (s : ℝ) => T s x) Tt t) (hHt : HasDerivAt (fun (s : ℝ) => I.Hm hΦ m κ T s x) Ht t) (hξt : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (I.xiMK m k) (ξt k) t) (hχt : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (fun (s : ℝ) => I.chiTilde hΦ m κ k s x) (χt k) t) (hGt : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (fun (s : ℝ) => G I hΦ m T (lIdx β I.Λ m k) s x) (Gt k) t) (hTx : HasFDerivAt (T t) LT x) (hHx : HasFDerivAt (I.Hm hΦ m κ T t) LH x) (hχx : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasFDerivAt (I.chiTilde hΦ m κ k t) (Lχ k) x) (hGx : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t y) (LG k) x) : deriv (fun (s : ℝ) => I.ansatz hΦ m κ T s x) t + (fderiv ℝ (I.ansatz hΦ m κ T t) x) b = Tt + Ht + ∑ k ∈ xiMKNearSupportFinset I m t ρ, (ξt k * Homogenization.vecDot (I.chiTilde hΦ m κ k t x) (G I hΦ m T (lIdx β I.Λ m k) t x) + I.xiMK m k t * (Homogenization.vecDot (χt k) (G I hΦ m T (lIdx β I.Λ m k) t x) + Homogenization.vecDot (I.chiTilde hΦ m κ k t x) (Gt k))) + (LT b + ∑ k ∈ xiMKNearSupportFinset I m t ρ, I.xiMK m k t * (Homogenization.vecDot ((Lχ k) b) (G I hΦ m T (lIdx β I.Λ m k) t x) + Homogenization.vecDot (I.chiTilde hΦ m κ k t x) ((LG k) b)) + LH b)

Source-level material differentiation of the line-2 ansatz. The finite cutoff support is chosen uniformly near t; the hypotheses are the pointwise time and space derivatives needed by the product rule. The source identity e.timecomp.0 follows by substituting its transport identities and the separate equation for Hm.