Exact zero-amplitude initial layer. Homogeneous classical uniqueness and the actual T forcing recursion are used, independently of negative times.

theorem AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectZeroData.relative_zero_data_classical_solution {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ∀ (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), F t x = 0) : IsClassicalSol (streamVel φ) κ F (fun (x : Homogenization.Vec 2) => 0) fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectZeroData.relative_zero_data_solution_is_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {κ : ℝ} (hκ : 0 < κ) {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θ) (t : ℝ) : 0 ≤ t → θ t = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_TIterates_zero_of_zero_data {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} (hκprev : 0 < κprev) {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θprev) {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev (fun (x : Homogenization.Vec 2) => 0) θprev T) (i : ℕ) : i ≤ Nstar β → ∀ (t : ℝ), 0 ≤ t → T i t = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_datum_zero_of_amplitude_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} {ν : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hν : 0 < ν) (hsol : IsClassicalSol (streamVel φ) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) (hmean : Homogenization.MeanZeroOn unitCube g) (hS : √ν * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θ t) x) = 0) : g = 0

A vanishing previous-scale dissipation amplitude forces the datum to zero by the mean-zero classical energy lower bound.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_defect_zero_of_zero_data {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {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) (hg : g = 0) (hHm : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq (I.Hm hΦ m κ (T (Nstar β)) s)) ≤ 0) : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => θm s x - I.ansatz hΦ m κ (T (Nstar β)) s x) = 0

Exact actual error vanishes at small positive times when the datum is zero and the proved Hm bound has zero amplitude.