Analytic estimates under the stream-regularity and diffusivity-recursion estimates, with an explicit initial derivative trace.

theorem AVenhance.Infra.Section4.ThetaAnalyticTrace.theta_initial_trace_l2_sq_le {B R : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hB : 0 ≤ B) (hTrace : ∀ (w : List (Fin 2)), √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ B * (↑w.length.factorial / R ^ w.length)) : l2NormSq θ₀ ≤ B ^ 2

theorem AVenhance.Infra.Section4.theta_homogeneous_gradient_energy_le_of_initial_l2_sq {κ B : ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hInitial : l2NormSq θ₀ ≤ B ^ 2) : (κ * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θ t)) ≤ B ^ 2

The homogeneous differentiated energy identity bounds the order-zero space-time gradient using only the initial L² trace. This is the base datum used by the coordinate profile; no time-uniform scalar norm enters.

theorem AVenhance.Infra.Section4.ThetaAnalyticTrace.theta_gradient_only_order_zero_bound_of_initial_l2_sq {κ B : ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hκ : 0 < κ) (hB : 0 ≤ B) (hInitial : l2NormSq θ₀ ≤ B ^ 2) : thetaAnalyticInductionLevel θ κ 0 ≤ B

theorem AVenhance.Infra.Section4.ThetaAnalyticTrace.theta_gradient_only_order_zero_bound_of_gradient_energy {κ B : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hκ : 0 < κ) (hB : 0 ≤ B) (hzero : κ * thetaWordSpaceTimeGradientEnergy θ [] ≤ B ^ 2) : thetaAnalyticInductionLevel θ κ 0 ≤ B

theorem AVenhance.Infra.Section4.theta_analytic_positive_energy_bound_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 : ℝ} (hc : 0 < c) (_hC : c < C) (hB : 0 < B) (hR : 0 < 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) θ₀ θ) (n : ℕ) : 1 ≤ n → thetaEnergyLevel θ (I.kappaSeq κ M (m - 1)) n ≤ 2 * B * ↑n.factorial * thetaAnalyticRadius c (epsilon β I.Λ (m - 1)) (gamma β) R ^ n

Positive-order analytic energy bounds from the initial trace and a gradient-only order-zero datum. The trace is required only at positive order; the zeroth level is supplied separately by hzero.