L2 estimate for the actual endpoint source in the Hm material telescope. Unlike Hmr, this endpoint uses q_r (not q_{r+1}); the terminal r=Jcut needs only one spatial derivative, within the corrected mixed budget.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_budget {β : ℝ} (I : Ingredients β) {r : ℕ} (hr : r ≤ Jcut β) : 1 ≤ Nstar β - 2 * r

The endpoint spatial derivative fits at every correction level, including Jcut. No two-spatial-letter estimate is consumed at the terminal level.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_spatial_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) (x : Homogenization.Vec 2) (hDtx : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) : hmEndpoint I hΦ m κ T r t x = ∑ i : Fin 2, ∑ n ∈ Finset.range (Nstar β), ∑ j : Fin 2, ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x i * I.qMNR κ m n r t j k

Exact spatial derivative expansion of the endpoint, with q_r.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_L2_of_Amnr_gradient {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ))) (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hAmnrGrad : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialGradientTensor I hΦ m κ T n r) 2 μ ≤ ENNReal.ofReal A) (hGradEntryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r z.1 x i j k) z.2 p) μ) (hDifferentiable : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => hmEndpoint I hΦ m κ T r z.1 z.2) 2 μ ≤ ∑ n ∈ Finset.range (Nstar β), ENNReal.ofReal (8 * (4 * Real.pi ^ 2 * C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ n * (8 * tau β I.Λ m) ^ r) * A)

The q coefficient is discharged from the physical paper-scale estimate; the upstream AMNR gradient amplitude remains an abstract scalar.