The actual positive-time endpoint source at the physical amplitude scale. All regularity is proved from the T iterates. The quantitative gradient profile is the output of EndpointJets, including the terminal one-letter level.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_L2_of_gradient_profile {β C₀ CA K L S : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm ν : ℝ} (hκm : 0 < κm) (hν : 0 < ν) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm ν g θprev T) (hz : I.Czeta ≤ C₀) (hCA : 0 ≤ CA) (hL : 0 ≤ L) (hS : 0 ≤ S) (hRatio : epsilon β I.Λ m ^ 2 / (κm * tau β I.Λ m) ≤ 1) (hTime : 8 * tau β I.Λ m / tauP β I.Λ m ≤ 1) (hX : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm ≤ K * ν) {r : ℕ} (hr : r ≤ Jcut β) (hAmnr : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialGradientTensor I hΦ m κm (T (Nstar β)) n r) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (CA * S * (epsilon β I.Λ m ^ 2 / κm) / √ν * L * (tauP β I.Λ m)⁻¹ ^ r)) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => hmEndpoint I hΦ m κm (T (Nstar β)) r z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (↑(Nstar β) * (8 * (4 * Real.pi ^ 2 * C₀) * CA * K * √ν * L * S))

The physical endpoint is L2 with amplitude sqrt(kappa_prev)LS, at every level through Jcut. No initial-time Amnr or Hm value is used.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_material_source_L2_of_gradient_profiles {β C₀ CA K L S : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm ν : ℝ} (hκm : 0 < κm) (hν : 0 < ν) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm ν g θprev T) (hz : I.Czeta ≤ C₀) (hCA : 0 ≤ CA) (hL : 0 ≤ L) (hS : 0 ≤ S) (hRatio : epsilon β I.Λ m ^ 2 / (κm * tau β I.Λ m) ≤ 1) (hTime : 8 * tau β I.Λ m / tauP β I.Λ m ≤ 1) (hX : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm ≤ K * ν) (hAmnr : ∀ r ≤ Jcut β, ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialGradientTensor I hΦ m κm (T (Nstar β)) n r) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (CA * S * (epsilon β I.Λ m ^ 2 / κm) / √ν * L * (tauP β I.Λ m)⁻¹ ^ r)) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => hmEndpoint I hΦ m κm (T (Nstar β)) (Jcut β) z.1 z.2 - hmEndpoint I hΦ m κm (T (Nstar β)) 0 z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (2 * (↑(Nstar β) * (8 * (4 * Real.pi ^ 2 * C₀) * CA * K * √ν * L * S)))

The actual material source is the terminal endpoint minus the zeroth endpoint. Both estimates use only one spatial letter at their respective levels.