Space-time bounds for the primitive/material pairings in l.V. Conditional material inputs refer to the actual material derivative fields.

theorem AVenhance.Infra.Section4.iterate_timeCube_isOpen : IsOpen timeCube

Openness of the energy cell, independent of corrector tensors.

theorem AVenhance.Infra.Section4.iterate_matrix_product_entry_bound (Q G : Matrix (Fin 2) (Fin 2) ℝ) {D B : ℝ} (hQ : ∀ (i j : Fin 2), |Q i j| ≤ D) (hG : ∀ (i j : Fin 2), |G i j| ≤ B) (i j : Fin 2) : |(Q * G) i j| ≤ 2 * D * B

Dimension-two entrywise control for the matrix products in Err4,1/2.

theorem AVenhance.Infra.Section4.iterate_material_equation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F u₀ u) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : amnrMaterial b u t x = κ * spaceLap (u t) x + F t x

The material equation comes from the actual classical PDE.