The explicit one-mode corrector solves its parabolic equation.

theorem AVenhance.Infra.Section3.zetaMK_eq_zero_before_support {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) (ht : t < (↑k - 2 / 3) * tau β I.Λ m) : I.zetaMK m k t = 0

The small cutoff of a mode vanishes before its translated support starts.

theorem AVenhance.Infra.Section3.corrTime_eq_zero_before_support {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (ht : t < (↑k - 2 / 3) * tau β I.Λ m) : I.corrTime κ m k t = 0

The memory coefficient is zero before the support of its forcing begins.

theorem AVenhance.Infra.Section3.chiMK_component_contDiff_two {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (j : Fin 2) : ContDiff ℝ 2 fun (p : ℝ × Homogenization.Vec 2) => I.chiMK κ m k p.1 p.2 j

Each scalar component of chiMK is jointly C² in time and space.

theorem AVenhance.Infra.Section3.ChiMKCorrector.spaceLap_zero_function (x : Homogenization.Vec 2) : spaceLap (fun (x : Homogenization.Vec 2) => 0) x = 0

theorem AVenhance.Infra.Section3.ChiMKCorrector.chiMK_spaceLap_of_zero_component {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) (hzero : (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) = fun (x : Homogenization.Vec 2) => 0) : spaceLap (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) x = -(4 * Real.pi ^ 2 / epsilon β I.Λ m ^ 2) * I.chiMK κ m k t x j

theorem AVenhance.Infra.Section3.ChiMKCorrector.chiMK_spaceLap_one_active {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hk : k % 4 = 1) : spaceLap (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x = -(4 * Real.pi ^ 2 / epsilon β I.Λ m ^ 2) * I.chiMK κ m k t x 1

theorem AVenhance.Infra.Section3.ChiMKCorrector.chiMK_spaceLap_three_active {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hk : k % 4 = 3) : spaceLap (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x = -(4 * Real.pi ^ 2 / epsilon β I.Λ m ^ 2) * I.chiMK κ m k t x 0

theorem AVenhance.Infra.Section3.chiMK_component_spaceLap_eigen {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : spaceLap (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) x = -(4 * Real.pi ^ 2 / epsilon β I.Λ m ^ 2) * I.chiMK κ m k t x j

Every single-mode corrector component is a spatial Laplacian eigenfunction with its shear frequency.

theorem AVenhance.Infra.Section3.chiMK_component_hasDerivAt {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : HasDerivAt (fun (s : ℝ) => I.chiMK κ m k s x j) (-(I.zetaProd m k t - 4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * I.corrTime κ m k t) * uShear β I.Λ m k x j) t

The time derivative of one explicit corrector component.

theorem AVenhance.Infra.Section3.ChiMKCorrector.spaceGrad_zero_of_fun_eq_zero {f : Homogenization.Vec 2 → ℝ} (hf : f = fun (x : Homogenization.Vec 2) => 0) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad f x i = 0

theorem AVenhance.Infra.Section3.chiMK_transport_identity {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : ∑ i : Fin 2, uShear β I.Λ m k x i * (Homogenization.basisVec j i + spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) x i) = uShear β I.Λ m k x j

The active shear is orthogonal to the corrector gradient, so its transport of e_j + ∇χ_j is exactly its jth component.

theorem AVenhance.Infra.Section3.chiMK_component_hasCorrectorPDE {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (j : Fin 2) (t : ℝ) (x : Homogenization.Vec 2) : HasDerivAt (fun (s : ℝ) => I.chiMK κ m k s x j) (κ * spaceLap (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) x - I.zetaProd m k t * ∑ i : Fin 2, uShear β I.Λ m k x i * (Homogenization.basisVec j i + spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y j) x i)) t

The explicit component solves the parabolic equation in direction e_j.

theorem AVenhance.Infra.Section3.chiMK_component_zero_before_support {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (j : Fin 2) (t : ℝ) (x : Homogenization.Vec 2) (ht : t < (-(2 / 3) + ↑k) * tau β I.Λ m) : I.chiMK κ m k t x j = 0

The explicit corrector vanishes before its support interval begins.

theorem AVenhance.Infra.Section3.chiMK_isCorrectorSol {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (j : Fin 2) : I.IsCorrectorSol κ m k (Homogenization.basisVec j) fun (t : ℝ) (x : Homogenization.Vec 2) => I.chiMK κ m k t x j

The explicit single-mode corrector satisfies the equation and initial cutoff condition.

theorem AVenhance.Infra.Section3.chiMK_component_isBoundedCorrectorSol {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (j : Fin 2) : (ContDiff ℝ 2 fun (p : ℝ × Homogenization.Vec 2) => I.chiMK κ m k p.1 p.2 j) ∧ (∃ (B : ℝ), ∀ (t : ℝ) (x : Homogenization.Vec 2), |I.chiMK κ m k t x j| ≤ B) ∧ I.IsCorrectorSol κ m k (Homogenization.basisVec j) fun (t : ℝ) (x : Homogenization.Vec 2) => I.chiMK κ m k t x j

The explicit chiMK component has all of the existence-side properties in the statement of the diffusivity-recursion estimate: joint C² regularity, a global bound, and the corrector equation with its prescribed past support.