Right-limit initial defect for the Section 5 ansatz

The ansatz at time zero depends on the arbitrary negative-time extension of an iterate. This file proves its required initial defect as s → 0⁺. The only input data are the literal diffusivity bounds conclusion and the positive-time Hm bound from half-cell bound; continuity and the oscillatory corrector bound are proved here.

theorem AVenhance.Infra.Section5.Integration.PartIInitial.initial_sqrt_l2NormSq_le_of_abs_le {f g : Homogenization.Vec 2 → ℝ} (hg : Continuous g) (hfg : ∀ (x : Homogenization.Vec 2), |f x| ≤ g x) : √(l2NormSq f) ≤ √(l2NormSq g)

theorem AVenhance.Infra.Section5.Integration.PartIInitial.initial_sqrt_l2NormSq_const_mul {c : ℝ} (hc : 0 ≤ c) (f : Homogenization.Vec 2 → ℝ) : √(l2NormSq fun (x : Homogenization.Vec 2) => c * f x) = c * √(l2NormSq f)

theorem AVenhance.Infra.Section5.Integration.PartIInitial.tNstar_classical_solution {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {θ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) : ∃ (F : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) κprev F θ₀ (T (Nstar β))

theorem AVenhance.Infra.Section5.Integration.PartIInitial.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.Integration.PartIInitial.classical_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.Integration.PartIInitial.tIterates_zero_of_zero_data {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ 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.Integration.PartIInitial.initial_gamma_lt_one {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : gamma β < 1

theorem AVenhance.Infra.Section5.Integration.PartIInitial.initial_ansatz_scale_bound {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {K e em A : ℝ} (hK : 1 ≤ K) (he : 0 < e) (he1 : e ≤ 1) (hem : 0 < em) (hA0 : 0 ≤ A) (hA : A ≤ K * em ^ (-gamma β)) (hemK : em ≤ K * e ^ q β) : A * em / (2 * Real.pi) * e ^ (-(1 + gamma β / 2)) ≤ K ^ 2 * e ^ delta β

Abstract-real scale conversion, kept local to avoid importing the diffusivity bounds wrapper.

theorem AVenhance.Infra.Section5.Integration.PartIInitial.initial_chi_const_eq {a e κ : ℝ} (ha : 0 < a) (he : 0 < e) (hκ : 0 < κ) : (4 * Real.pi ^ 2 * κ / e ^ 2)⁻¹ * |2 * Real.pi * a * e| = a * e ^ 2 / κ * e / (2 * Real.pi)

theorem AVenhance.Infra.Section5.Integration.PartIInitial.continuous_pair_difference_l2_at_initial {b b' : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ κ' : ℝ} {Fforce Gforce Fsol Gsol : ℝ → Homogenization.Vec 2 → ℝ} {f₀ : Homogenization.Vec 2 → ℝ} (hF : IsClassicalSol b κ Fforce f₀ Fsol) (hG : IsClassicalSol b' κ' Gforce f₀ Gsol) (η : ℝ) : 0 < η → ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => Fsol s x - Gsol s x) < η

theorem AVenhance.Infra.Section5.Integration.PartIInitial.continuous_classical_gradient_l2_at_initial {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : IsClassicalSol b κ F θ₀ T) (η : ℝ) : 0 < η → ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(gradNormSq (spaceGrad (T s))) < √(gradNormSq (spaceGrad θ₀)) + η

theorem AVenhance.Infra.Section5.Integration.PartIInitial.corrector_l2_bound_by_gradient {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κ : ℝ} (hκ : 0 < κ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : √(l2NormSq fun (x : Homogenization.Vec 2) => I.ansatz hΦ m κ T t x - T t x - I.Hm hΦ m κ T t x) ≤ 8 * chiSup I κ m * √(gradNormSq (spaceGrad (T t)))

theorem AVenhance.Infra.Section5.Integration.chiSup_analytic_scale_of_A5 {β : ℝ} (I : Ingredients β) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) {κ : ℝ} (hκ : 0 < κ) (hPerm : κ ∈ permittedInterval β I.Λ M) (hM : 1 ≤ M) {C₀ c C : ℝ} (_hCzeta : I.Czeta ≤ C₀) (_hCxi : I.Cxi ≤ C₀) (_hChat : I.Chat ≤ C₀) (_hpermissible : κ ∈ permissibleSet β I.Λ) (hc : 0 < c) (_hcC : c < C) (hA5 : (∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) ∧ ∀ (j : ℕ), 2 ≤ j → j < M → c * epsilon β I.Λ (j - 1) ^ (4 * delta β) ≤ epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ∧ epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ≤ C * epsilon β I.Λ (j - 1) ^ (4 * delta β)) {R : ℝ} (_hR : 0 < R) (hRscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) : 0 < I.kappaSeq κ M m ∧ chiSup I (I.kappaSeq κ M m) m * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2)) ≤ max (max 1 (min c (1 / 2))⁻¹) (1 + Ingredients.supergeoConstant β) ^ 2 * epsilon β I.Λ (m - 1) ^ delta β

the coefficient scale, conditional on the literal two-part diffusivity bounds conclusion. The terminal index uses the already-proved one-sided l_recurse_top endpoint estimate.

theorem AVenhance.Infra.Section5.Integration.partI_initial_right_limit_of_A5_and_Hm_of_positive_data {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) {κ : ℝ} (hκ : 0 < κ) (hPerm : κ ∈ permittedInterval β I.Λ M) (hM : 1 ≤ M) {C₀ c C R CH : ℝ} (hCzeta : I.Czeta ≤ C₀) (hCxi : I.Cxi ≤ C₀) (hChat : I.Chat ≤ C₀) (hpermissible : κ ∈ permissibleSet β I.Λ) (hc : 0 < c) (hcC : c < C) (hA5 : (∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) ∧ ∀ (j : ℕ), 2 ≤ j → j < M → c * epsilon β I.Λ (j - 1) ^ (4 * delta β) ≤ epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ∧ epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ≤ C * epsilon β I.Λ (j - 1) ^ (4 * delta β)) {θ₀ : Homogenization.Vec 2 → ℝ} {θm θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {κm : ℝ} (hNpos : 0 < √(l2NormSq θ₀)) (hθm : IsClassicalSol (streamVel (Φ m)) κm (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θm) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T) (hR : 0 < R) (hRscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, θ₀ x = 0) (hanalytic : IsThetaAnalytic R θ₀) (hCH : 0 ≤ CH) (hHm : ∀ t ∈ Set.Ioc 0 1, √(l2NormSq (I.Hm hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t)) ≤ CH * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => θm s x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s x) ≤ (CH + 2 + 8 * max (max 1 (min c (1 / 2))⁻¹) (1 + Ingredients.supergeoConstant β) ^ 2 * (√2 + 1)) * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)

the right-limit input to step-down part (i), under the exact diffusivity bounds conclusion and the scalar Hm bound. The oscillatory corrector contributes the sharper ε_(m-1)^(4δ) through q(1−γ)−1−γ/2=4δ; it is weakened to the common ε_(m-1)^δ scale in the result.

theorem AVenhance.Infra.Section5.Integration.partI_initial_zero_defect_of_A5_and_Hm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) {κ c C CH : ℝ} (hc : 0 < c) (hA5 : (∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) ∧ ∀ (j : ℕ), 2 ≤ j → j < M → c * epsilon β I.Λ (j - 1) ^ (4 * delta β) ≤ epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ∧ epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ≤ C * epsilon β I.Λ (j - 1) ^ (4 * delta β)) {θ₀ : Homogenization.Vec 2 → ℝ} {θm θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {κm : ℝ} (hNzero : √(l2NormSq θ₀) = 0) (hκmpos : 0 < κm) (hθm : IsClassicalSol (streamVel (Φ m)) κm (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θm) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T) (hHm : ∀ t ∈ Set.Ioc 0 1, √(l2NormSq (I.Hm hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t)) ≤ CH * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) (t : ℝ) : t ∈ Set.Ioc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x) = 0

Zero-data counterpart of the right-limit estimate. Classical uniqueness makes both temperature solutions and every T iterate vanish; the supplied Hm estimate then forces the remaining ansatz term to vanish in L².