The order-zero A/q endpoint is the homogenized flux defect applied to the flow-averaged pulled gradient.

theorem AVenhance.Infra.Section5.Gbar_eq_finite_support {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Gbar I hΦ m T t x = ∑ l ∈ ⋯.toFinset, I.hatXiML m l t • G I hΦ m T l t x

At a fixed time, the flow average in Gbar is a finite sum over the support of the large-scale cutoffs.

theorem AVenhance.Infra.Section5.Jhat_sub_Kmat_eq_LMN_qMNR_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (κ t : ℝ) : I.Jhat κ m t - I.Kmat κ m t = ∑ n ∈ Finset.range (Nstar β), I.LMN κ m n t • I.qMNR κ m n 0 t

The instantaneous Jhat minus the time-smoothed Kmat is the sum of the L_{m,n} q_{m,n,0} coefficients.

The base endpoint is not -div((JHat - K) GDot) for the base tensor (corrected form, left F_lᵀ); instead it is given by LeftJacobian.variantA_hmEndpoint_zero (Section5/LeftJacobian/BaseFlux.lean): hmEndpoint … 0 = -div(Σ_l ξ̂_l F_lᵀ (JHat - K) F_l ∇T).