Exact relative initial-layer contract from the two separately proved corrector and positive-time Hm estimates, including zero dissipation amplitude.

theorem AVenhance.Infra.Section5.RelativeError.relative_initialLayer_from_estimates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ ν : ℝ} (hκ : 0 < κ) (hν : 0 < ν) {g : Homogenization.Vec 2 → ℝ} {θm θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol (streamVel (Φ m)) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θm) (hp : IsClassicalSol (streamVel (Φ (m - 1))) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κ ν g θprev T) (hmean : Homogenization.MeanZeroOn unitCube g) {Ccorr CH : ℝ} (hCorrector : √(l2NormSq fun (x : Homogenization.Vec 2) => ∑' (k : ℤ), Integration.ansatzSummand I hΦ m κ (T (Nstar β)) k 0 x) ≤ Ccorr * epsilon β I.Λ (m - 1) ^ delta β * (√ν * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev t) x))) (hHm : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq (I.Hm hΦ m κ (T (Nstar β)) s)) ≤ CH * epsilon β I.Λ (m - 1) ^ delta β * (√ν * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev t) x))) : Integration.InitialLayerContract I hΦ m κ θm T (Ccorr + CH + 1) (√ν * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev t) x))

Assembly of the literal relative initial-layer contract. The component estimates remain explicit, distinct from the family-level producer.