Relative Hm initial-layer control from gradient-only iterate spatial jets. The endpoint recursion checks the mixed budget through terminal Jcut.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_uniform_of_jets (β C₀ Cg Cl : ℝ) (hCg : 0 ≤ Cg) (hCl : 1 ≤ Cl) : ∃ (CH : ℝ), 0 ≤ CH ∧ ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → ∀ (S : ℝ), 0 ≤ S → (∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube)) ≤ ENNReal.ofReal (Cg * S / √(I.kappaSeq κ M (m - 1)) * (Cl * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length)) → ∀ t ∈ Set.Ioc 0 (tauPP β I.Λ m / 2), √(l2NormSq (I.Hm hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t)) ≤ CH * epsilon β I.Λ (m - 1) ^ delta β * S

The relative Hm bound is produced from upstream spatial jets, with abstract amplitude S >= 0. No Hm-source bound is assumed.