Source-specific completion of the Section 5.1 ansatz residual (corrected form).

FrozenResidualPointwiseData is the corrected-form pointwise calculus record LeftJacobian.ResidualPointwiseData, and frozen_source_residual_identity proves the named-slot sourceResidualIdentity (ten slot names, §9.4 sourceErrorD) from it (LeftJacobian.frozen_variantA_source_residual_identity).

@[reducible, inline]

abbrev AVenhance.Infra.Section5.FrozenResidualPointwiseData {β : ℝ} (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 residual proof (corrected form).

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.frozen_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 : FrozenResidualPointwiseData I hΦ m hm κm κprev θ₀ θprev T hT t ht x ρ hρ) : sourceResidualIdentity I hΦ m κm κprev T t x

The complete source-form Section 5.1 residual from the T-iterate and the pointwise calculus data (corrected form, ten slot names).