Adapter to the actual spatial divergence-gradient tensor. Import this module directly: HmBounds already imports the AmnrBounds facade.

theorem AVenhance.Infra.Section4.amnr_product_measure_eq_timeCube : (MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube) = MeasureTheory.volume.restrict timeCube

The two integration measures in the Amnr and Hm APIs coincide.

theorem AVenhance.Infra.Section4.amnr_hm_second_derivative_budget {β : ℝ} {r : ℕ} (hr : r ∈ Finset.range (Jcut β)) : 2 ≤ Nstar β - 2 * r

Two spatial letters fit the source budget at every Hm summation level.

theorem AVenhance.Infra.Section4.amnr_actual_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n r a : ℕ) (hbudget : a + r ≤ Nstar β) (i j k : Fin 2) : ContDiffOn ℝ (↑a) (fun (z : AmnrSpace) => I.Amnr hΦ m κm n (T (Nstar β)) r z.1 z.2 i j k) (Set.Ioi 0 ×ˢ Set.univ)

Actual iterate solutions give the finite joint regularity required by spatial slicing; no mixed estimate is assumed here.

theorem AVenhance.Infra.Section4.amnr_hm_hessian_entry_measurable_of_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n r : ℕ) (hreg : ∀ (i j k : Fin 2), ContDiffOn ℝ 2 (fun (z : AmnrSpace) => I.Amnr hΦ m κ n T r z.1 z.2 i j k) (Set.Ioi 0 ×ˢ Set.univ)) (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)

Finite actual joint regularity supplies the Hessian entry measurability argument required by the Hm consumer, on its exact physical cell.

theorem AVenhance.Infra.Section4.amnr_hm_hessian_of_mixed_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n r : ℕ) {B : ℝ} (hreg : ∀ (i j k : Fin 2), ContDiffOn ℝ 2 (fun (z : AmnrSpace) => I.Amnr hΦ m κ n T r z.1 z.2 i j k) (Set.Ioi 0 ×ˢ Set.univ)) (hBound : ∀ (p i : Fin 2), MeasureTheory.eLpNorm (fun (z : AmnrSpace) (a j k : Fin 2) => amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord [p, i] 0) (fun (y : AmnrSpace) => I.Amnr hΦ m κ n T r y.1 y.2 a j k) z) 2 ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube)) ≤ ENNReal.ofReal B) : MeasureTheory.eLpNorm (amnrSpatialDivergenceGradientTensor I hΦ m κ T n r) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (16 * B)

A spatial specialization of the mixed tensor bound supplies the hAmnrHess input of hm_bounds_of_flowFTC_and_pAmnr, with its exact four-index carrier. Joint C² regularity is a primitive slicing condition; amnr_actual_contDiffOn proves it for the actual iterates.