The actual positive-time Hm material equation. Every calculus premise of the finite telescope is discharged from the actual T iteration.

theorem AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectMaterialEquation.stDiv_eq_vecDiv {F : ST → Homogenization.Vec 2} {t : ℝ} {x : Homogenization.Vec 2} (hF : DifferentiableAt ℝ F (t, x)) : stDiv F (t, x) = vecDiv (fun (y : Homogenization.Vec 2) => F (t, y)) x

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Aq_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm κprev g θprev T) (n r q : ℕ) (i j k : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : ST) => I.Amnr hΦ m κm n (T (Nstar β)) r z.1 z.2 i j k * I.qMNR κm m n q z.1 j k) (Set.Ioi 0 ×ˢ Set.univ)

Actual A/q fluxes are jointly smooth on positive times, independently of whether the q index is r or r+1.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Aq_sum_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm κprev g θprev T) (N r q : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : ST) (i : Fin 2) => ∑ n ∈ Finset.range N, ∑ j : Fin 2, ∑ k : Fin 2, I.Amnr hΦ m κm n (T (Nstar β)) r z.1 z.2 i j k * I.qMNR κm m n q z.1 j k) (Set.Ioi 0 ×ˢ Set.univ)

Finite actual A/q flux sums have open-time joint regularity.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_material_equation {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm κprev g θprev T) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : deriv (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) t + (fderiv ℝ (I.Hm hΦ m κm (T (Nstar β)) t) x) (streamVel (Φ (m - 1)) t x) = hmEndpoint I hΦ m κm (T (Nstar β)) (Jcut β) t x - hmEndpoint I hΦ m κm (T (Nstar β)) 0 t x

The actual Hm satisfies the endpoint material equation at every positive time; all differentiability inputs of the telescope are proved internally.