base energy at the later start("The coarse diffusivity satisfies ...",

"Poincaré at 9166–9190 gives ...") and §6 item 11. For j = laterStart β Λ R < M:

• κ_j ≥ c R^{p₊} (from the diffusivity lower bound κ_j ≥ c₀ ε_j^{β+γ}, the minimality of j, and, for j = 1, the radius bound R ≤ 1/(√2 π));
• κ_j ‖∇θ_j‖² ≥ c R^{p₊} ‖g‖² from the energy identity and Poincaré.

The κ conjunct is stated for nonzero data (0 < l2NormSq g →): for g = 0 and large R the index j = 1 is the later start while R^{p₊} is unbounded, so it cannot hold uniformly.

theorem AVenhance.Infra.Section5.RelativeError.a_mul_eps_pow_eq {β : ℝ} {Λ m : ℕ} (hx : 0 < epsilon β Λ m) (γ : ℝ) : a β Λ m * epsilon β Λ m ^ (2 + γ) = epsilon β Λ m ^ (β + γ)

a_m ε_m^{2+γ} = ε_m^{β+γ}.

theorem AVenhance.Infra.Section5.RelativeError.inv_sqrt_two_mul_pi_le_one : 1 / (√2 * Real.pi) ≤ 1

1/(√2 π) ≤ 1.

theorem AVenhance.Infra.Section5.RelativeError.kappa_lower_of_cases {c₀ e₁ p R Kj eJ : ℝ} {j : ℕ} (hc₀ : 0 < c₀) (he₁ : 0 < e₁) (hp : 0 < p) (hR : 0 < R) {h : ℝ} (hKj : c₀ * eJ ≤ Kj) (hj1 : j = 1 → eJ = e₁) (hj2 : 2 ≤ j → (1 / 2) ^ h * R ^ p ≤ eJ) (hj0 : 1 ≤ j) (hR1 : j = 1 → R ≤ 1) : min (c₀ * e₁) (c₀ * (1 / 2) ^ h) * R ^ p ≤ Kj

The abstract lower bound for κ_j at the later start, in terms of a constant c₁.

theorem AVenhance.Infra.Section5.RelativeError.later_base_energy (β C₀ : ℝ) (hβ : 6 / 5 ≤ β) (Λ : ℕ) : 2 ^ 7 ≤ Λ → ∃ (c : ℝ), 0 < c ∧ ∀ (I : Ingredients β), I.Λ = Λ → I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (R : ℝ), 0 < R → laterStart β I.Λ R < M → ∀ (g : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) g → IsZ2Periodic g → Homogenization.MeanZeroOn unitCube g → IsThetaAnalytic R g → ∀ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (laterStart β I.Λ R))) (I.kappaSeq κ M (laterStart β I.Λ R)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ → (0 < l2NormSq g → c * R ^ pPlus β ≤ I.kappaSeq κ M (laterStart β I.Λ R)) ∧ c * R ^ pPlus β * l2NormSq g ≤ I.kappaSeq κ M (laterStart β I.Λ R) * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θ t) x

Item 11: base energy at the later start, with c after β, C₀, Λ and before κ, M, R, g. The κ conjunct is for nonzero data (see the module docstring).