Discharge the stream-regularity/diffusivity-recursion data and convert theta derivative estimates to the order-zero coordinate profile.

theorem AVenhance.Infra.Section4.ThetaProfileDischarge.iterateSpatialWord_eq_classicalWordDerivative (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : iterateSpatialWord w f = classicalWordDerivative w f

theorem AVenhance.Infra.Section4.theta_A3_A5_data_of_frozen {β : ℝ} {M : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (hM : 1 ≤ M) (hPerm : κ ∈ permittedInterval β I.Λ M) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ c < C ∧ (∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) ∧ ∀ (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 β))

Stream-regularity and diffusivity-recursion data extracted from the conclusions. The second stream-regularity display and both diffusivity bounds are retained verbatim.

theorem AVenhance.Infra.Section4.theta_analytic_energy_bound_of_frozen_A3_A5 {β : ℝ} {M m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) (hmM : m ≤ M) {κ R : ℝ} (hR : 0 < R) (hPerm : κ ∈ permittedInterval β I.Λ M) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : IsThetaAnalytic R θ₀) {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel fun (t : ℝ) => Φ (m - 1) t) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ c < C ∧ ∀ (n : ℕ), thetaEnergyLevel θ (I.kappaSeq κ M (m - 1)) n ≤ 2 * √(l2NormSq θ₀) * ↑n.factorial * thetaAnalyticRadius c (epsilon β I.Λ (m - 1)) (gamma β) R ^ n

The original analytic energy bound with stream-regularity and diffusivity-recursion discharged by the conclusions. The diffusivity-recursion constants remain explicit outputs for downstream radius bookkeeping.

theorem AVenhance.Infra.Section4.ThetaProfileDischarge.theta_initial_trace_of_analytic {B R : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : IsThetaAnalytic R θ₀) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F θ₀ θ) (hB : √(l2NormSq θ₀) ≤ B) (hR : 0 < R) (w : List (Fin 2)) : √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ B * (↑w.length.factorial / R ^ w.length)

theorem AVenhance.Infra.Section4.ThetaProfileDischarge.theta_profile_source_radius_le {β c R C₀ : ℝ} {m : ℕ} (I : Ingredients β) (hscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) (hC₀ : 8 * max (thetaAnalyticRadiusBase c) 2 ≤ C₀) : 8 * thetaAnalyticRadius c (epsilon β I.Λ (m - 1)) (gamma β) R ≤ C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)

theorem AVenhance.Infra.Section4.theta_profile_radius_absorbed_by_source_constant {cProfile Cθ Csource Rflow C₀ : ℝ} (hTheta : 4 * max (thetaAnalyticRadiusBase cProfile) 2 ≤ Cθ) (hSource : iterateSourceConstant Csource Rflow Cθ ≤ C₀) : 8 * max (thetaAnalyticRadiusBase cProfile) 2 ≤ C₀

The source constant passed to the next estimate absorbs the analytic theta radius when Cθ is chosen from the diffusivity-recursion constant.

theorem AVenhance.Infra.Section4.theta_iterate_profile_of_initial_trace_A3_A5 {β : ℝ} {M m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) (hmM : m ≤ M) {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {c C B R C₀ : ℝ} (hc : 0 < c) (hC : c < C) (hB : 0 < B) (hR : 0 < R) (hRadius : 8 * max (thetaAnalyticRadiusBase c) 2 ≤ C₀) (hscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) (hzero : (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θ t)) ≤ B ^ 2) (hTrace : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ B * (↑w.length.factorial / R ^ w.length)) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (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 β))) (hsol : IsClassicalSol (streamVel fun (t : ℝ) => Φ (m - 1) t) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) : iterateCoordinateEnergyProfile θ (I.kappaSeq κ M (m - 1)) B (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0

Convert the generic analytic energy estimate into the order-zero profile required by the actual T upgrade. The only input from the initial datum is the explicit all-orders wordwise L² trace bound.

theorem AVenhance.Infra.Section4.ThetaProfileDischarge.theta_iterate_profile_of_zero_data {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ L : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θ) : iterateCoordinateEnergyProfile θ κ 0 L 0