e.left.to.show with the composed-analyticity hypothesis discharged (route A)

left_to_show_conditional_of_bounds replaces the hypothesis hAn of left_to_show_conditional by the two SOURCE estimates it is derived from in 8588–8600 and 7060–7075: the all-orders L∞_t L²_x part of e.Tm.reg.upgrade (TmRegUpgradeLinfL2) and the flow bound e.flow.for.ergodic on supp ξ_{m,k} (FlowForErgodicBound), through H² ⊂ L∞, l.product and Proposition 10528 (AnalyticBridge.hasCoordinateAnalyticL1Bounds_of_bounds); the resulting amplitude loss is ε_{m-1}^{-(6+3γ)}.

theorem AVenhance.Infra.Section5.LeftToShow.AssemblyBounds.amplitude_le {e γ A' A'' θ : ℝ} (he : 0 < e) (hA : A' ≤ A'') (hθ : 0 ≤ θ) : A' * (e ^ (1 + γ / 2)) ^ (-6) * θ ≤ A'' * e ^ (-(6 + 3 * γ)) * θ

theorem AVenhance.Infra.Section5.LeftToShow.left_to_show_conditional_of_bounds (β C₀ A : ℝ) (hA : 1 ≤ A) : ∃ (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)⁻¹ → AnalyticBridge.TmRegUpgradeLinfL2 A (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) θ₀ (T (Nstar β)) → (∀ t ∈ Set.Ioo 0 1, ∀ (k : ℤ), Odd k → I.xiMK m k t ≠ 0 → AnalyticBridge.FlowForErgodicBound A (epsilon β I.Λ (m - 1)) (I.xFlow hΦ m (lIdx β I.Λ m k) t)) → |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 (additive), conditional only on source estimates for T_{m-1} and the flows: e.Tm.reg.upgrade (n = 0 L²_tH¹ part hT0, and all orders L∞_tL²_x hTall), e.barf.cascade (n = 0, ℓ = 1, hDt) and e.flow.for.ergodic on supp ξ_{m,k} (hFlow), all with one constant A ≥ 1 (they weaken as A grows).