e.left.to.show: assembly

Source enhance.tex 8271–8882. The exact four-term identity ergodic_break_up with J = J_m^{κ_m}, the vanishing fourth term (⟨⟨J_m^{κ_m}⟩⟩ = κ_{m-1} I), and the three scaled term estimates ergodic_space_kill (ε_{m-1}^{500}), ergodic_break_up_second_scaled and ergodic_break_up_last (ε_{m-1}^{2δ}). Only the ADDITIVE form is proved.

theorem AVenhance.Infra.Section5.LeftToShow.left_to_show_conditional (β C₀ A P : ℝ) (hA : 0 < A) (hP : 0 ≤ P) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) x) ≤ A * √(l2NormSq θ₀) → √(spaceTimeGradNormSq (materialGrad (streamVel (Φ (m - 1))) (T (Nstar β)))) ≤ A * epsilon β I.Λ (m - 1) ^ (3 * delta β) * (√(I.kappaSeq κ M (m - 1)))⁻¹ * √(l2NormSq θ₀) * (tauP β I.Λ m)⁻¹ → (∀ t ∈ Set.Ioo 0 1, ∀ (k : ℤ), Odd k → I.xiMK m k t ≠ 0 → ∀ (i j : Fin 2), Ergodic.HasCoordinateAnalyticL1Bounds (fun (y : Homogenization.Vec 2) => ↑(spaceGrad (T (Nstar β) t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) i * spaceGrad (T (Nstar β) t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) j)) (A * epsilon β I.Λ (m - 1) ^ (-P) * l2NormSq θ₀) (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / A)) → |I.kappaSeq κ M m * spaceTimeGradNormSq (leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β))) - I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) x| ≤ C * epsilon β I.Λ (m - 1) ^ (2 * delta β) * l2NormSq θ₀

e.left.to.show (8271–8293, proof 8294–8882), additive form, conditional on the §4 estimates for T_{m-1} = T (Nstar β) (proved elsewhere): e.Tm.reg.upgrade (n = 0), e.barf.cascade (n = 0, ℓ = 1) and the composed analyticity e.ass.f.anal.flows of ∂_iT_{m-1}∂_jT_{m-1} ∘ X_{m-1,l_k} used for l.flow.averages; the constants A, P are those estimates' constants (they depend on β only). hAn is required only where ξ_{m,k}(t) ≠ 0 (the source flow bounds e.Xm.bound.* hold only on supp ξ_{m,k}, 7066–7075); every hypothesis weakens as A grows, so A = max of the three upstream constants; P = 2 + γ suffices for the Leibniz product of the L² bounds . The bridge from the L²_x bounds on T to the L¹ bounds on ∂_iT ∂_jT ∘ X is not written in the source (SOURCE_GAP-lite).