The exact selected-flow spatial gradient of the line-2 ansatz.

theorem AVenhance.Infra.Section5.SelectedAnsatzSpatial.chiMK_eq_zero_of_not_odd {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (hk : ¬Odd k) (t : ℝ) : I.chiMK κ m k t = 0

theorem AVenhance.Infra.Section5.SelectedAnsatzSpatial.chiTilde_eq_zero_of_not_odd {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (hk : ¬Odd k) (t : ℝ) : I.chiTilde hΦ m κ k t = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.ansatz_spaceGrad_selected {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) {LT LH : Homogenization.Vec 2 →L[ℝ] ℝ} (Lχ LG : ℤ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (hT : HasFDerivAt (T t) LT x) (hH : HasFDerivAt (I.Hm hΦ m κm T t) LH x) (hχ : ∀ k ∈ ⋯.toFinset, HasFDerivAt (I.chiTilde hΦ m κm k t) (Lχ k) x) (hG : ∀ k ∈ ⋯.toFinset, HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t y) (LG k) x) (i : Fin 2) : spaceGrad (I.ansatz hΦ m κm T t) x i = ∑ k ∈ ⋯.toFinset with Odd k, I.xiMK m k t * ((gradMatrix (I.chiTilde hΦ m κm k t) x).mulVec (G I hΦ m T (lIdx β I.Λ m k) t x) i + G I hΦ m T (lIdx β I.Λ m k) t x i) + (spaceGrad (T t) x i - ∑ k ∈ ⋯.toFinset with Odd k, I.xiMK m k t * G I hΦ m T (lIdx β I.Λ m k) t x i) + ∑ k ∈ ⋯.toFinset with Odd k, I.xiMK m k t * ∑ j : Fin 2, I.chiTilde hΦ m κm k t x j * spaceGrad (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m k) t y j) x i + spaceGrad (I.Hm hΦ m κm T t) x i

The gradient of the ansatz, reorganized into its selected odd flows. The mismatch flux is kept explicitly as ∇T - Σ_{k odd} ξ_{m,k} G_{l_k}; together with the selected corrector fluxes this is exactly the line-2 gradient.