: the candidate base flux Σ_n A⁺_{n,0} q_{n,0} and the order-zero endpoint of the H_m telescope (the corrected-form analogue of HmBaseFluxIdentity).

theorem AVenhance.Infra.Section5.LeftJacobian.base_term_contraction (L ξ : ℝ) (W q : Matrix (Fin 2) (Fin 2) ℝ) (g : Homogenization.Vec 2) (i : Fin 2) : ∑ j : Fin 2, ∑ k : Fin 2, -L * (ξ * (W j i * ∑ p : Fin 2, W k p * g p)) * q j k = -(ξ * L * W.transpose.mulVec (q.mulVec (W.mulVec g)) i)

One (n, l) term of the base flux: contracting F_{ji} (F ∇T)_k against q_{jk} gives (Fᵀ q F ∇T)_i, the j of F_{ji} contracting with the row of q.

theorem AVenhance.Infra.Section5.LeftJacobian.sum_comm_fin_fin_finset {α : Type u_1} (S : Finset α) (f : Fin 2 → Fin 2 → α → ℝ) : ∑ j : Fin 2, ∑ k : Fin 2, ∑ l ∈ S, f j k l = ∑ l ∈ S, ∑ j : Fin 2, ∑ k : Fin 2, f j k l

theorem AVenhance.Infra.Section5.LeftJacobian.amnrBasePlus_qMNR_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : (fun (i : Fin 2) => ∑ n ∈ Finset.range (Nstar β), ∑ j : Fin 2, ∑ k : Fin 2, amnrBasePlus I hΦ m κm n T t x i j k * I.qMNR κm m n 0 t j k) = -∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t x).transpose.mulVec ((I.Jhat κm m t - I.Kmat κm m t).mulVec ((I.flowGrad hΦ m l t x).mulVec (spaceGrad (T t) x)))

theorem AVenhance.Infra.Section5.LeftJacobian.vecDiv_neg_eq {V : Homogenization.Vec 2 → Homogenization.Vec 2} (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => -V y) x = -vecDiv V x

theorem AVenhance.Infra.Section5.LeftJacobian.variantA_hmEndpoint_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : hmEndpoint I hΦ m κm T 0 t x = -vecDiv (fun (y : Homogenization.Vec 2) => ∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t y).transpose.mulVec ((I.Jhat κm m t - I.Kmat κm m t).mulVec ((I.flowGrad hΦ m l t y).mulVec (spaceGrad (T t) y)))) x

The order-zero endpoint of the H_m telescope under the corrected-form base tensor (the base, Amnr_zero_eq_amnrBasePlus): the negative divergence of Σ_l ξ̂_l F_lᵀ (JHat - K) F_l ∇T.