Exact right-limit initial error at positive abstract amplitude. The zero amplitude branch is handled separately using actual zero-data solutions.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initialLayer_of_positive_amplitude
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κ ν : ℝ}
(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)
{B D S : ℝ}
(hS : 0 < S)
(hCorrector :
√(l2NormSq fun (x : Homogenization.Vec 2) => ∑' (k : ℤ), Integration.ansatzSummand I hΦ m κ (T (Nstar β)) k 0 x) ≤ B * S)
(hHm : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq (I.Hm hΦ m κ (T (Nstar β)) s)) ≤ D * S)
:
The actual error, rather than the ansatz-to-datum norm, satisfies the exact initial-layer contract after absorbing a positive right-limit slack.