: the end-to-end residual identity for the names.

This mirrors Section5/ResidualCompletion.lean (frozen_source_residual_identity) with the corrected-form pieces switched in:

• variantA_source_material_equation (source transport equation with V_tr and d⁺),
• variantA_ansatz_material_equation_of_source (source-generic ansatz material equation),
• the unchanged named diffusion expansion,
• variantA_residual_identity_sel_of_expansions (literal-name identity (36)),
• residualIdentityPlus_of_sel (repaired identity (38), needs T t smooth).

Now the I.sMat, I.Amnr · 0 are the corrected-form bodies by rfl (sMat_eq_sMatPlus, Amnr_zero_eq_amnrBasePlus); the former switch-later hypotheses are gone. frozen_variantA_source_residual_identity states the result with the slot names.

structure AVenhance.Infra.Section5.LeftJacobian.ResidualPointwiseData {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) (ρ : ℝ) (hρ : 0 < ρ) : Type

Pointwise calculus data for the corrected-form source residual. The fields are those of FrozenResidualPointwiseData that remain needed, with the corrected-form replacements: hAvg is derived from hVecGlobal/hIterateGlobal (via sMat_eq_sMatPlus), hTail/hBase feed the source material equation, hr46/hDE feed the divergence split of V_tr + d⁺ + e, hSmooth gives the C¹ regularity of T t and the regrouping (36) → (38), and hTx, hHx, hG are derived from the global/odd-support derivative fields.

• Dt : ℕ → ℝ

  Time derivatives of the Hm recursion terms at the residual evaluation point.

• LHm : ℕ → Homogenization.Vec 2 →L[ℝ] ℝ

  Spatial differentials of the Hm recursion terms at the residual evaluation point.

• hDt (r : ℕ) : r ∈ Finset.range (Jcut β) → HasDerivAt (fun (s : ℝ) => I.Hmr hΦ m κm (T (Nstar β)) r s x) (self.Dt r) t
• hDx (r : ℕ) : r ∈ Finset.range (Jcut β) → HasFDerivAt (I.Hmr hΦ m κm (T (Nstar β)) r t) (self.LHm r) x
• hA (r : ℕ) : r ∈ Finset.range (Jcut β) → ∀ (n : ℕ) (i j k : Fin 2) (z : ST), 0 < z.1 → DifferentiableAt ℝ (fun (w : ST) => I.Amnr hΦ m κm n (T (Nstar β)) r w.1 w.2 i j k) z
• hPair (r : ℕ) : r ∈ Finset.range (Jcut β) → ∀ (a : AmnrPairIndex) (z : ST), 0 < z.1 → DifferentiableAt ℝ (amnrPairFlux I hΦ m κm (T (Nstar β)) r a) z
• hFlux (r : ℕ) : r ∈ Finset.range (Jcut β) → ContDiffAt ℝ 2 (amnrPairFluxSum I hΦ m (Nstar β) κm (T (Nstar β)) r) (t, x)
• hEndNext (r : ℕ) : r ∈ Finset.range (Jcut β) → DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κm (T (Nstar β)) (r + 1)) (t, x)
• hEnd (r : ℕ) : r ∈ Finset.range (Jcut β) → DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κm (T (Nstar β)) r) (t, x)
• hTail : DifferentiableAt ℝ (terminalTail I hΦ m κm (T (Nstar β)) t) x
• hBase : DifferentiableAt ℝ (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 (Nstar β) t) y)))) x
• hTtime : HasDerivAt (fun (s : ℝ) => T (Nstar β) s x) (deriv (fun (s : ℝ) => T (Nstar β) s x) t) t
• hHtime : HasDerivAt (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) (deriv (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) t) t
• hXi (k : ℤ) : k ∈ xiMKNearSupportFinset I m t ρ → HasDerivAt (I.xiMK m k) (deriv (I.xiMK m k) t) t
• Lχ : ℤ → ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

  Joint time-space differentials of the transported corrector components.

• LG : ℤ → ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

  Joint time-space differentials of the transported temperature gradients.

• hChiJoint (k : ℤ) : k ∈ xiMKNearSupportFinset I m t ρ → HasFDerivAt (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => I.chiTilde hΦ m κm k s y) (self.Lχ k) (t, x)
• hGJoint (k : ℤ) : k ∈ xiMKNearSupportFinset I m t ρ → HasFDerivAt (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) (lIdx β I.Λ m k) s y) (self.LG k) (t, x)
• hr46 : DifferentiableAt ℝ (r46Flux I hΦ m κm (T (Nstar β)) t) x
• hDE : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => sourceErrorDPlus I hΦ m κm (T (Nstar β)) t y + iterateError I hΦ m κm κprev T t y) x
• hSmooth : ContDiff ℝ (↑⊤) (T (Nstar β) t)
• hHGlobal (y : Homogenization.Vec 2) : HasFDerivAt (I.Hm hΦ m κm (T (Nstar β)) t) (fderiv ℝ (I.Hm hΦ m κm (T (Nstar β)) t) y) y
• hChiGlobal (k : ℤ) : k ∈ ⋯.toFinset → ∀ (y : Homogenization.Vec 2), HasFDerivAt (I.chiTilde hΦ m κm k t) (fderiv ℝ (I.chiTilde hΦ m κm k t) y) y
• hGGlobal (k : ℤ) : k ∈ ⋯.toFinset → ∀ (y : Homogenization.Vec 2), HasFDerivAt (fun (z : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) (lIdx β I.Λ m k) t z) (fderiv ℝ (fun (z : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) (lIdx β I.Λ m k) t z) y) y
• hCorrectorFlux (q : { k : ℤ // Odd k }) : q ∈ ⋯.toFinset → ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => correctorFlux I hΦ m κm (↑q) t y i j) (fderiv ℝ (fun (y : Homogenization.Vec 2) => correctorFlux I hΦ m κm (↑q) t y i j) x) x
• hGodd (q : { k : ℤ // Odd k }) : HasFDerivAt (fun (y : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) (lIdx β I.Λ m ↑q) t y) (fderiv ℝ (fun (y : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) (lIdx β I.Λ m ↑q) t y) x) x
• LM : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

  Spatial differential of the diffusion-weighted gradient mismatch.

• LC : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

  Spatial differential of the cutoff-weighted corrector gradient flux.

• LHflux : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

  Spatial differential of the Hm flux contribution to the residual.

• hMismatch : HasFDerivAt (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κm t y).mulVec (spaceGrad (T (Nstar β) t) y - ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • G I hΦ m (T (Nstar β)) (lIdx β I.Λ m ↑q) t y)) self.LM x
• hChiFlux : HasFDerivAt (fun (y : Homogenization.Vec 2) => ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • (diffusionMatrix I hΦ m κm t y).mulVec (chiGradG I hΦ m κm (T (Nstar β)) (↑q) t y)) self.LC x
• hHmFlux : HasFDerivAt (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κm t y).mulVec (spaceGrad (I.Hm hΦ m κm (T (Nstar β)) t) y)) self.LHflux x
• hVecGlobal (y : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (z : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t z).mulVec (spaceGrad (T (Nstar β) t) z)) y
• hIterateGlobal (y : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (z : Homogenization.Vec 2) => iterateError I hΦ m κm κprev T t z) y
• hVecDiv : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => vecDiv (fun (z : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t z).mulVec (spaceGrad (T (Nstar β) t) z)) y) x
• hIterateDiv : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => vecDiv (fun (z : Homogenization.Vec 2) => iterateError I hΦ m κm κprev T t z) y) x
• hAnsatz : ContDiffAt ℝ 2 (I.ansatz hΦ m κm (T (Nstar β)) t) x

theorem AVenhance.Infra.Section5.LeftJacobian.Residual.spaceGrad_add_residual' {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : spaceGrad (fun (y : Homogenization.Vec 2) => f y + g y) x = spaceGrad f x + spaceGrad g x

theorem AVenhance.Infra.Section5.LeftJacobian.variantA_source_residual_identity_sel {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) (ρ : ℝ) (hρ : 0 < ρ) (R : ResidualPointwiseData I hΦ m hm κm κprev θ₀ θprev T hT t ht x ρ hρ) : residualIdentitySel I hΦ m κm (T (Nstar β)) (sourceErrorDPlus I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) (streamVel (Φ m)) t x

corrected-form literal-name residual identity (36) for the names, given the pointwise calculus data (sMat, Amnr).

theorem AVenhance.Infra.Section5.LeftJacobian.variantA_source_residual_identity {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) (ρ : ℝ) (hρ : 0 < ρ) (R : ResidualPointwiseData I hΦ m hm κm κprev θ₀ θprev T hT t ht x ρ hρ) : residualIdentityPlus I hΦ m κm (T (Nstar β)) (sourceErrorDPlus I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) (streamVel (Φ m)) t x

corrected-form repaired residual identity (38) for the names, given the pointwise calculus data (sMat, Amnr).

theorem AVenhance.Infra.Section5.LeftJacobian.frozen_variantA_source_residual_identity {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) (ρ : ℝ) (hρ : 0 < ρ) (R : ResidualPointwiseData I hΦ m hm κm κprev θ₀ θprev T hT t ht x ρ hρ) : sourceResidualIdentity I hΦ m κm κprev T t x

The named-slot Section 5.1 residual identity (corrected form, ten slot names): sourceResidualIdentity with the slot bodies of Terms.lean and the §9.4 sourceErrorD.