Source-scale reduction for the HTilde_m. The cutoff is exactly range (Jcut β), as fixed by the corrected index conventions. The analytic term estimates are kept separate from the finite-sum and differentiation arguments below.

theorem AVenhance.Infra.Section4.hm_transport_absorb {H L D : ℝ} (hH : 0 < H) (htransport : H ^ 2 ≤ 2 * L * D * H) : H ≤ 2 * L * D

Absorption step in the source's flow FTC argument: a nonnegative supremum satisfying H² ≤ 2 L D H is bounded by 2 L D.

theorem AVenhance.Infra.Section4.hm_transport_cell_sup_le {f : ℝ → ℝ} {cell : Set ℝ} {H L D : ℝ} (hH : 0 < H) (hattain : ∃ t ∈ cell, f t = H) (hupper : ∀ t ∈ cell, f t ≤ H) (hFTC : ∀ t ∈ cell, f t ^ 2 ≤ 2 * L * D * H) (t : ℝ) : t ∈ cell → f t ≤ 2 * L * D

Cellwise conclusion of the source's transported-energy FTC estimate. hFTC is the inequality obtained after the flow change of variables, Cauchy--Schwarz in time, and the source derivative bound; this lemma performs the supremum absorption and then bounds every time in the cell.

theorem AVenhance.Infra.Section4.hmr_eq_spatial_derivative_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) : I.Hmr 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 + 1) t j k

Expand the divergence defining Hmr into the finite sum of spatial derivatives of Amnr times the time-only qMNR entries.

noncomputable def AVenhance.Infra.Section4.amnrSpatialDivergenceGradientTensor {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n r : ℕ) (z : ℝ × Homogenization.Vec 2) : Fin 2 → Fin 2 → Fin 2 → Fin 2 → ℝ

The mixed second spatial derivative of Amnr selected by the divergence index of Hmr.

Equations

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

noncomputable def AVenhance.Infra.Section4.hmrGradientQbase {β : ℝ} (I : Ingredients β) (C₀ : ℝ) (m r : ℕ) : ℝ

Common paper-scale factor in the corrected qMNR estimate.

Equations

• AVenhance.Infra.Section4.hmrGradientQbase I C₀ m r = 4 * Real.pi ^ 2 * C₀ * (AVenhance.a β I.Λ m ^ 2 * AVenhance.epsilon β I.Λ m ^ 2) * (8 * AVenhance.tau β I.Λ m) ^ (r + 1)

theorem AVenhance.Infra.Section4.hmr_spaceGrad_eq_second_spatial_derivative_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (hD1 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) (t : ℝ) (x : Homogenization.Vec 2) (p : Fin 2) : spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t x) x p = ∑ i : Fin 2, ∑ n ∈ Finset.range (Nstar β), ∑ j : Fin 2, ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x p * I.qMNR κ m n (r + 1) t j k

Differentiate the exact Hmr expansion once more in space. This is the source identity behind the (k,ell)=(2,0) instance of p.Amnr.

theorem AVenhance.Infra.Section4.hmr_spaceGrad_components_eLpNorm_le_of_pAmnr_qMNR {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hAmnrHess : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (amnrSpatialDivergenceGradientTensor I hΦ m κ T n r) 2 μ ≤ ENNReal.ofReal A) (hHessEntryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p) μ) (hD1 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) (p : Fin 2) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2 p) 2 μ ≤ 8 * ↑(Nstar β) * ENNReal.ofReal (hmrGradientQbase I C₀ m r * A)

Each output component of the gradient is bounded by the finite (i,n,j,k) sum supplied by the (k,ell)=(2,0) AMNR estimate.

theorem AVenhance.Infra.Section4.eLpNorm_vec2_le_sum {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → Homogenization.Vec 2) (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm f 2 μ ≤ MeasureTheory.eLpNorm (fun (x : α) => ∑ p : Fin 2, ‖f x p‖) 2 μ

Pointwise coordinate dominance gives this vector-valued L² comparison.

theorem AVenhance.Infra.Section4.eLpNorm_sum_norm_vec2_le_of_coordinate_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → Homogenization.Vec 2) (hf : MeasureTheory.AEStronglyMeasurable f μ) {B : ENNReal} (hcoordinate : ∀ (p : Fin 2), MeasureTheory.eLpNorm (fun (x : α) => f x p) 2 μ ≤ B) : MeasureTheory.eLpNorm (fun (x : α) => ∑ p : Fin 2, ‖f x p‖) 2 μ ≤ 2 * B

The sum of coordinate norms has the corresponding L² bound.

theorem AVenhance.Infra.Section4.eLpNorm_vec2_le_of_coordinate_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → Homogenization.Vec 2) (hf : MeasureTheory.AEStronglyMeasurable f μ) {B : ENNReal} (hcoordinate : ∀ (p : Fin 2), MeasureTheory.eLpNorm (fun (x : α) => f x p) 2 μ ≤ B) : MeasureTheory.eLpNorm f 2 μ ≤ 2 * B

The vector-valued L² norm is controlled by its two coordinate bounds.

theorem AVenhance.Infra.Section4.hmr_component_count_identity (N : ℕ) (x y : ℝ) : 2 * (8 * ↑N * ENNReal.ofReal (x * y)) = ENNReal.ofReal (16 * ↑N * y * x)

Convert the finite component count in the previous lemma to the paper's real-valued scale.

theorem AVenhance.Infra.Section4.hmr_spaceGrad_eLpNorm_le_of_componentBounds {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hGradientMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) μ) (hComponentBound : ∀ (p : Fin 2), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2 p) 2 μ ≤ 8 * ↑(Nstar β) * ENNReal.ofReal (hmrGradientQbase I C₀ m r * A)) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 μ ≤ ENNReal.ofReal (16 * ↑(Nstar β) * A * hmrGradientQbase I C₀ m r)

Assemble the two component estimates into the vector-valued ∇Hmr estimate.

theorem AVenhance.Infra.Section4.hmr_spaceGrad_eLpNorm_le_of_pAmnr_qMNR {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hAmnrHess : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (amnrSpatialDivergenceGradientTensor I hΦ m κ T n r) 2 μ ≤ ENNReal.ofReal A) (hHessEntryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p) μ) (hGradientMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) μ) (hD1 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 μ ≤ ENNReal.ofReal (16 * ↑(Nstar β) * A * hmrGradientQbase I C₀ m r)

Termwise spacetime L² bound for the actual gradient ∇Hmr. The AMNR input is the (k,ell)=(2,0) tensor estimate. The corrected qMNR norm bound controls each time-dependent coefficient, and the small mode ratio replaces its individual n weight by the common upper factor.

noncomputable def AVenhance.Infra.Section4.amnrSpatialGradientTensor {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n r : ℕ) (z : ℝ × Homogenization.Vec 2) : Fin 2 → Fin 2 → Fin 2 → Fin 2 → ℝ

The p.Amnr tensor bound controls each scalar spatial derivative entry.

Equations

• AVenhance.Infra.Section4.amnrSpatialGradientTensor I hΦ m κ T n r z i j k p = AVenhance.spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r z.1 x i j k) z.2 p

theorem AVenhance.Infra.Section4.hm_spaceGrad_eq_sum_hmr {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) (t : ℝ) : (spaceGrad fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T t x) = ∑ r ∈ Finset.range (Jcut β), spaceGrad fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t x

Differentiation in x commutes with the finite Hm sum.

theorem AVenhance.Infra.Section4.hm_gradient_eLpNorm_le_of_hmr {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) {B : ℝ} (hB : 0 ≤ B) (hterm : ∀ r ∈ Finset.range (Jcut β), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal B) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (↑(Jcut β) * B)

The gradient L² bound for Hm reduces to the corresponding termwise source-scale estimates at indices r < Jcut.

theorem AVenhance.Infra.Section4.hm_gradient_source_scale_of_hmr {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) {E δ C θ Kinvhalf : ℝ} (hE : 0 ≤ E) (hC : 0 ≤ C) (hθ : 0 ≤ θ) (hKinv : 0 ≤ Kinvhalf) (hterm : ∀ r ∈ Finset.range (Jcut β), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (C * E ^ (4 * δ) * Kinvhalf * θ)) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (↑(Jcut β) * C * E ^ (4 * δ) * Kinvhalf * θ)

Source-scale form of the spacetime gradient reduction, retaining the corrected summand range r < Jcut.

theorem AVenhance.Infra.Section4.hm_bounds_of_flowFTC_and_termwise_gradient {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) {f H L D E δ C₀ C₁ θ Kinvhalf : ℝ} (hNorm : ∀ t ∈ Set.Icc 0 1, MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T t x) 2 (MeasureTheory.volume.restrict unitCube) = ENNReal.ofReal f) (hH : 0 < H) (hattain : ∃ t ∈ Set.Icc 0 1, f = H) (hupper : ∀ t ∈ Set.Icc 0 1, f ≤ H) (hFTC : ∀ t ∈ Set.Icc 0 1, f ^ 2 ≤ 2 * L * D * H) (hscale : 2 * L * D ≤ C₀ * E ^ δ * θ) (hE : 0 ≤ E) (hC₁ : 0 ≤ C₁) (hθ : 0 ≤ θ) (hKinv : 0 ≤ Kinvhalf) (hGradHmr : ∀ r ∈ Finset.range (Jcut β), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (C₁ * E ^ (4 * δ) * Kinvhalf * θ)) : (∀ t ∈ Set.Icc 0 1, MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T t x) 2 (MeasureTheory.volume.restrict unitCube) ≤ ENNReal.ofReal (C₀ * E ^ δ * θ)) ∧ MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (↑(Jcut β) * C₁ * E ^ (4 * δ) * Kinvhalf * θ)

Conditional p.Hm conclusion with the source FTC step isolated. The hFTC premise is precisely the transported squared-L² inequality on the whole time interval; flow_comp_hasDerivAt_of_fderiv supplies its pointwise material derivative once the source regularity is instantiated.

theorem AVenhance.Infra.Section4.hm_bounds_of_flowFTC_and_pAmnr {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) {C₀ C₁ A E δ θ Kinvhalf f H L D : ℝ} (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hAmnrHess : ∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (amnrSpatialDivergenceGradientTensor I hΦ m κ T n r) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal A) (hHessEntryMeas : ∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p) (MeasureTheory.volume.restrict timeCube)) (hGradientMeas : ∀ r ∈ Finset.range (Jcut β), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) (MeasureTheory.volume.restrict timeCube)) (hD1 : ∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ r ∈ Finset.range (Jcut β), ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) (hGradientScale : ∀ r ∈ Finset.range (Jcut β), 16 * ↑(Nstar β) * A * hmrGradientQbase I C₀ m r ≤ C₁ * E ^ (4 * δ) * Kinvhalf * θ) (hNorm : ∀ t ∈ Set.Icc 0 1, MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T t x) 2 (MeasureTheory.volume.restrict unitCube) = ENNReal.ofReal f) (hH : 0 < H) (hattain : ∃ t ∈ Set.Icc 0 1, f = H) (hupper : ∀ t ∈ Set.Icc 0 1, f ≤ H) (hFTC : ∀ t ∈ Set.Icc 0 1, f ^ 2 ≤ 2 * L * D * H) (hscale : 2 * L * D ≤ C₀ * E ^ δ * θ) (hE : 0 ≤ E) (hC₁ : 0 ≤ C₁) (hθ : 0 ≤ θ) (hKinv : 0 ≤ Kinvhalf) : (∀ t ∈ Set.Icc 0 1, MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T t x) 2 (MeasureTheory.volume.restrict unitCube) ≤ ENNReal.ofReal (C₀ * E ^ δ * θ)) ∧ MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (↑(Jcut β) * C₁ * E ^ (4 * δ) * Kinvhalf * θ)

The p.Amnr (k,ell)=(2,0) bounds and corrected qMNR estimate provide the termwise gradient input to the conditional p.Hm assembly. The transported FTC inequality remains an explicit premise because its endpoint and flow measure-preservation steps are not consequences of p.Amnr alone.